[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general fe8b9fccb3 25/25: Merge pull request #636 fr
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general fe8b9fccb3 25/25: Merge pull request #636 from dominique-unruh/qrhl-tool |
|
Date: |
Mon, 28 Feb 2022 07:58:46 -0500 (EST) |
branch: elpa/proof-general
commit fe8b9fccb3690178be7fc455202c941c4c674ac3
Merge: df19c7ba0e 360b6c24e3
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>
Merge pull request #636 from dominique-unruh/qrhl-tool
Support for qrhl-tool theorem prover
---
Makefile.devel | 2 +-
README.md | 1 +
doc/PG-adapting.texi | 2 +-
doc/ProofGeneral.texi | 2 -
generic/proof-autoloads.el | 523 ++++++++++++++++++++-----------
generic/proof-site.el | 1 +
qrhl/qrhl-input-25.el | 753 ++++++++++++++++++++++++++++++++++++++++++++
qrhl/qrhl-input.el | 763 +++++++++++++++++++++++++++++++++++++++++++++
qrhl/qrhl.el | 140 +++++++++
9 files changed, 2007 insertions(+), 180 deletions(-)
diff --git a/Makefile.devel b/Makefile.devel
index f244798bdc..d0bb67a979 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -246,7 +246,7 @@ distclean: devclean clean
#
autoloads: $(EL)
@echo "***** MAKING AUTOGENERATED AUTOLOADS ****"
- $(BATCHEMACS) -eval '(setq autoload-package-name "proof"
generated-autoload-file "$(PWD)/generic/proof-autoloads.el")' -f
batch-update-autoloads generic/ lib/ coq/
+ $(BATCHEMACS) -eval '(setq autoload-package-name "proof"
generated-autoload-file "$(PWD)/generic/proof-autoloads.el")' -f
batch-update-autoloads generic/ lib/ coq/ qrhl/
############################################################
#
diff --git a/README.md b/README.md
index b4aa2e8be3..71ba70d5e2 100644
--- a/README.md
+++ b/README.md
@@ -132,6 +132,7 @@ Supported proof assistants:
* [Coq](https://coq.inria.fr/)
* [EasyCrypt](https://www.easycrypt.info/)
* [PhoX](https://raffalli.eu/phox/)
+* [qrhl-tool](https://github.com/dominique-unruh/qrhl-tool/#readme)
Proof General used to support other proof assistants, but those
instances are no longer maintained nor available in the MELPA package:
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 1dda289af5..ae36a00f72 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3305,7 +3305,7 @@ in the @code{proof-assistants} setting.
@c TEXI DOCSTRING MAGIC: proof-assistants
@defvar proof-assistants
Choice of proof assistants to use with Proof General.@*
-A list of symbols chosen from: @samp{coq} @samp{easycrypt} @samp{phox}
@samp{pgshell} @samp{pgocaml} @samp{pghaskell}.
+A list of symbols chosen from: @samp{coq} @samp{easycrypt} @samp{phox}
@samp{qrhl} @samp{pgshell} @samp{pgocaml} @samp{pghaskell}.
If nil, the default will be ALL available proof assistants.
Each proof assistant defines its own instance of Proof General,
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index a566a50092..f7748846f0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2706,8 +2706,6 @@ Show a buffer of all the shortcuts available.
Insert each Unicode character into a buffer.@*
Lets you see which characters are available for literal display
in your Emacs font.
-
-(fn)
@end deffn
@node Selecting suitable fonts
@section Selecting suitable fonts
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index d2ab935747..8090aa0c94 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -17,30 +17,72 @@
(provide 'proof-autoloads)
-;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (24631 49612 444031
-;;;;;; 796000))
+;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (0 0 0 0))
;;; Generated autoloads from ../coq/coq.el
-(autoload 'coq-pg-setup "../coq/coq" "\
+(autoload 'coq-pg-setup "../coq/coq" nil nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq" '("auto-adapt-printing-width" "build-list-id-from-string" "coq-"
"count-not-intersection" "hide-additional-subgoals" "is-not-split-vertic"
"last-coq-error-location" "mod" "notation-print-kinds-table" "printing-depth"
"proof-" "reqkinds-kinds-table" "time-commands")))
-\(fn)" nil nil)
+;;;***
+
+;;;### (autoloads nil "../coq/coq-abbrev" "../coq/coq-abbrev.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-abbrev.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-abbrev" '("coq-" "holes-show-doc")))
;;;***
;;;### (autoloads nil "../coq/coq-autotest" "../coq/coq-autotest.el"
-;;;;;; (24208 57600 771957 35000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from ../coq/coq-autotest.el
-(autoload 'coq-autotest "../coq/coq-autotest" "\
+(autoload 'coq-autotest "../coq/coq-autotest" nil t nil)
+;;;***
+
+;;;### (autoloads nil "../coq/coq-compile-common"
"../coq/coq-compile-common.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-compile-common.el
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-compile-common" '("coq-" "number-of-cpus" "time-less-or-equal")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-db" "../coq/coq-db.el" (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-db.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-db" '("coq-" "filter-state-" "max-length-db")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-diffs" "../coq/coq-diffs.el" (0
+;;;;;; 0 0 0))
+;;; Generated autoloads from ../coq/coq-diffs.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-diffs" '("coq-")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-indent" "../coq/coq-indent.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-indent.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-indent" '("coq-")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-local-vars" "../coq/coq-local-vars.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-local-vars.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-local-vars" '("coq-")))
;;;***
-;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (24208
-;;;;;; 57600 775957 25000))
+;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (0 0
+;;;;;; 0 0))
;;; Generated autoloads from ../coq/coq-mode.el
(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode))
@@ -52,16 +94,71 @@ Major mode for Coq scripts.
\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-mode" '("coq-" "get-coq-library-directory")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-par-compile" "../coq/coq-par-compile.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-par-compile.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-par-compile" '("coq-" "split-list-at-predicate")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-seq-compile" "../coq/coq-seq-compile.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-seq-compile.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-seq-compile" '("coq-seq-")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-smie" "../coq/coq-smie.el" (0 0
+;;;;;; 0 0))
+;;; Generated autoloads from ../coq/coq-smie.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-smie" '("coq-")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-syntax" "../coq/coq-syntax.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-syntax.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-syntax" '("coq-" "develock-coq-font-lock-keywords")))
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-system" "../coq/coq-system.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-system.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-system" '("coq-")))
+
;;;***
-;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (24208
-;;;;;; 57600 787956 998000))
+;;;### (autoloads nil "../coq/coq-unicode-tokens"
"../coq/coq-unicode-tokens.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../coq/coq-unicode-tokens.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../coq/coq-unicode-tokens" '("coq-")))
+
+;;;***
+
+;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (0 0 0
+;;;;;; 0))
;;; Generated autoloads from ../lib/bufhist.el
(autoload 'bufhist-mode "../lib/bufhist" "\
Minor mode retaining an in-memory history of the buffer contents.
-Commands:\\<bufhist-minor-mode-map>
+If called interactively, enable Bufhist mode if ARG is positive,
+and disable it if ARG is zero or negative. If called from Lisp,
+also enable the mode if ARG is omitted or nil, and toggle it if
+ARG is `toggle'; disable the mode otherwise.
+
+Commands:\\<bufhist-mode-map>
\\[bufhist-prev] bufhist-prev go back in history
\\[bufhist-next] bufhist-next go forward in history
\\[bufhist-first] bufhist-first go to first item in history
@@ -80,14 +177,13 @@ If RINGSIZE is omitted or nil, the size defaults to
‘bufhist-ring-size’.
\(fn &optional READWRITE RINGSIZE)" t nil)
(autoload 'bufhist-exit "../lib/bufhist" "\
-Stop keeping ring history for current buffer.
+Stop keeping ring history for current buffer." t nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/bufhist" '("bufhist-")))
;;;***
-;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (24208 57600
-;;;;;; 787956 998000))
+;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (0 0 0 0))
;;; Generated autoloads from ../lib/holes.el
(autoload 'holes-set-make-active-hole "../lib/holes" "\
@@ -189,19 +285,27 @@ undoing on holes cannot make holes re-appear.
Complete abbrev by putting holes and indenting.
Moves point at beginning of expanded text. Put this function as
call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
-become holes.
-
-\(fn)" nil nil)
+become holes." nil nil)
(autoload 'holes-insert-and-expand "../lib/holes" "\
Insert S, expand it and replace #s and @{]s by holes.
\(fn S)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/holes" '("hole")))
+
+;;;***
+
+;;;### (autoloads nil "../lib/local-vars-list" "../lib/local-vars-list.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../lib/local-vars-list.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/local-vars-list" '("local-vars-list-")))
+
;;;***
;;;### (autoloads nil "../lib/maths-menu" "../lib/maths-menu.el"
-;;;;;; (24208 57600 787956 998000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from ../lib/maths-menu.el
(autoload 'maths-menu-mode "../lib/maths-menu" "\
@@ -210,19 +314,60 @@ Uses window system menus only when they can display
multilingual text.
Otherwise the menu-bar item activates the text-mode menu system.
This mode is only useful with a font which can display the maths repertoire.
+If called interactively, enable Maths-Menu mode if ARG is
+positive, and disable it if ARG is zero or negative. If called
+from Lisp, also enable the mode if ARG is omitted or nil, and
+toggle it if ARG is `toggle'; disable the mode otherwise.
+
\(fn &optional ARG)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/maths-menu" '("maths-menu-")))
+
+;;;***
+
+;;;### (autoloads nil "../lib/pg-fontsets" "../lib/pg-fontsets.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../lib/pg-fontsets.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/pg-fontsets" '("pg-fontsets-")))
+
+;;;***
+
+;;;### (autoloads nil "../lib/proof-compat" "../lib/proof-compat.el"
+;;;;;; (0 0 0 0))
+;;; Generated autoloads from ../lib/proof-compat.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/proof-compat" '("pg-custom-undeclare-variable")))
+
+;;;***
+
+;;;### (autoloads nil "../lib/span" "../lib/span.el" (0 0 0 0))
+;;; Generated autoloads from ../lib/span.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/span" '("fold-spans" "next-span" "prev-span" "set-span-" "span")))
+
;;;***
-;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (24208 57600 779957
-;;;;;; 17000))
+;;;### (autoloads nil "../qrhl/qrhl" "../qrhl/qrhl.el" (0 0 0 0))
+;;; Generated autoloads from ../qrhl/qrhl.el
+
+(let ((loads (get 'qrhl 'custom-loads))) (if (member '"../qrhl/qrhl" loads)
nil (put 'qrhl 'custom-loads (cons '"../qrhl/qrhl" loads))))
+
+(defvar qrhl-input-method "qrhl" "\
+Input method to use when editing qRHL proof scripts")
+
+(custom-autoload 'qrhl-input-method "../qrhl/qrhl" t)
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../qrhl/qrhl" '("qrhl-")))
+
+;;;***
+
+;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (0 0 0 0))
;;; Generated autoloads from pg-assoc.el
(autoload 'proof-associated-buffers "pg-assoc" "\
Return a list of the associated buffers.
-Some may be dead/nil.
-
-\(fn)" nil nil)
+Some may be dead/nil." nil nil)
(autoload 'proof-associated-windows "pg-assoc" "\
Return a list of the associated buffers windows.
@@ -233,36 +378,47 @@ argument ALL-FRAMES has the same meaning than for
\(fn &optional ALL-FRAMES)" nil nil)
(autoload 'proof-associated-frames "pg-assoc" "\
-Return the list of frames displaying at least one associated buffer.
+Return the list of frames displaying at least one associated buffer." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-assoc" '("proof-")))
;;;***
-;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (24208 57600
-;;;;;; 787956 998000))
+;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (0 0 0 0))
;;; Generated autoloads from ../lib/pg-dev.el
(autoload 'profile-pg "../lib/pg-dev" "\
-Configure Proof General for profiling. Use \\[elp-results] to see results.
+Configure Proof General for profiling. Use \\[elp-results] to see results." t
nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/pg-dev" '("elp-pack-number" "pg-" "unload-pg")))
+
+;;;***
+
+;;;### (autoloads nil "pg-autotest" "pg-autotest.el" (0 0 0 0))
+;;; Generated autoloads from pg-autotest.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-autotest" '("pg-autotest")))
;;;***
-;;;### (autoloads nil "pg-goals" "pg-goals.el" (24208 57600 779957
-;;;;;; 17000))
+;;;### (autoloads nil "pg-custom" "pg-custom.el" (0 0 0 0))
+;;; Generated autoloads from pg-custom.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-custom" '("completion-table" "favourites" "help-menu-entries" "keymap"
"maths-menu-enable" "menu-entries" "one-command-per-line" "pro" "quit-timeout"
"script-indent" "tags-program" "toolbar-entries" "unicode-tokens-enable"
"use-holes")))
+
+;;;***
+
+;;;### (autoloads nil "pg-goals" "pg-goals.el" (0 0 0 0))
;;; Generated autoloads from pg-goals.el
(autoload 'proof-goals-config-done "pg-goals" "\
-Initialise the goals buffer after the child has been configured.
+Initialise the goals buffer after the child has been configured." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-goals" '("pg-goals-" "proof-goals-mode")))
;;;***
-;;;### (autoloads nil "pg-movie" "pg-movie.el" (24208 57600 779957
-;;;;;; 17000))
+;;;### (autoloads nil "pg-movie" "pg-movie.el" (0 0 0 0))
;;; Generated autoloads from pg-movie.el
(autoload 'pg-movie-export "pg-movie" "\
@@ -282,10 +438,11 @@ Existing XML files are overwritten.
\(fn DIR EXTN)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-movie" '("pg-movie-")))
+
;;;***
-;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (24217 47839 196027
-;;;;;; 466000))
+;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (0 0 0 0))
;;; Generated autoloads from pg-pamacs.el
(autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -333,10 +490,18 @@ This macro also extends the `proof-assistant-settings'
list.
\(fn NAME VAL &rest ARGS)" nil t)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-pamacs" '("deflocal" "defpg" "proof-" "undefpgcustom")))
+
;;;***
-;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (24208 57600 779957
-;;;;;; 17000))
+;;;### (autoloads nil "pg-pbrpm" "pg-pbrpm.el" (0 0 0 0))
+;;; Generated autoloads from pg-pbrpm.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-pbrpm" '("pbrpm-menu-desc" "pg-pbrpm-")))
+
+;;;***
+
+;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (0 0 0 0))
;;; Generated autoloads from pg-pgip.el
(autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -346,19 +511,16 @@ The list PGIPS may contain one or more PGIP packets,
whose contents are processe
\(fn PGIPS)" nil nil)
(autoload 'pg-pgip-maybe-askpgip "pg-pgip" "\
-Send an <askpgip> message to the prover if PGIP is supported.
-
-\(fn)" nil nil)
+Send an <askpgip> message to the prover if PGIP is supported." nil nil)
(autoload 'pg-pgip-askprefs "pg-pgip" "\
-Send an <askprefs> message to the prover.
+Send an <askprefs> message to the prover." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-pgip" '("pg-" "proof-assistant-idtables")))
;;;***
-;;;### (autoloads nil "pg-response" "pg-response.el" (24208 57600
-;;;;;; 783957 8000))
+;;;### (autoloads nil "pg-response" "pg-response.el" (0 0 0 0))
;;; Generated autoloads from pg-response.el
(autoload 'proof-response-mode "pg-response" "\
@@ -367,9 +529,7 @@ Responses from Proof Assistant
\(fn)" t nil)
(autoload 'proof-response-config-done "pg-response" "\
-Complete initialisation of a response-mode derived buffer.
-
-\(fn)" nil nil)
+Complete initialisation of a response-mode derived buffer." nil nil)
(autoload 'pg-response-maybe-erase "pg-response" "\
Erase the response buffer, according to confusing flag combinations.
@@ -421,33 +581,35 @@ and start at the first error.
(autoload 'pg-response-has-error-location "pg-response" "\
Return non-nil if the response buffer has an error location.
-See `pg-next-error-regexp'.
+See `pg-next-error-regexp'." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-response" '("pg-" "proof-")))
;;;***
-;;;### (autoloads nil "pg-user" "pg-user.el" (24230 6619 211624 483000))
+;;;### (autoloads nil "pg-user" "pg-user.el" (0 0 0 0))
;;; Generated autoloads from pg-user.el
(autoload 'proof-script-new-command-advance "pg-user" "\
Move point to a nice position for a new command, possibly inserting spaces.
Assumes that point is at the end of a command.
-No effect if `proof-next-command-insert-space' is nil.
-
-\(fn)" t nil)
+No effect if `proof-next-command-insert-space' is nil." t nil)
(autoload 'proof-goto-point "pg-user" "\
Assert or retract to the command at current position.
Calls `proof-assert-until-point' or `proof-retract-until-point' as
-appropriate.
+appropriate. With prefix argument RAW the omit proofs feature
+\(`proof-omit-proofs-option') is temporaily disabled to check all
+proofs in the asserted region.
-\(fn)" t nil)
+\(fn &optional RAW)" t nil)
(autoload 'proof-process-buffer "pg-user" "\
Process the current (or script) buffer, and maybe move point to the end.
+With prefix argument RAW the omit proofs feature (`proof-omit-proofs-option')
+is temporaily disabled to check all proofs in the asserted region.
-\(fn)" t nil)
+\(fn &optional RAW)" t nil)
(autoload 'proof-define-assistant-command "pg-user" "\
Define FN (docstring DOC): check if CMDVAR is set, then send BODY to prover.
@@ -469,30 +631,20 @@ It can also be used as a minor mode function: with ARG,
turn on iff ARG>0
\(fn &optional ARG)" nil nil)
-(autoload 'pg-slow-fontify-tracing-hint "pg-user" "\
-
-
-\(fn)" nil nil)
+(autoload 'pg-slow-fontify-tracing-hint "pg-user" nil nil nil)
(autoload 'pg-response-buffers-hint "pg-user" "\
\(fn &optional NEXTBUF)" nil nil)
-(autoload 'pg-jump-to-end-hint "pg-user" "\
-
-
-\(fn)" nil nil)
+(autoload 'pg-jump-to-end-hint "pg-user" nil nil nil)
(autoload 'pg-processing-complete-hint "pg-user" "\
-Display hint for showing end of locked region or processing complete.
-
-\(fn)" nil nil)
+Display hint for showing end of locked region or processing complete." nil nil)
(autoload 'pg-next-error-hint "pg-user" "\
-Display hint for locating error.
-
-\(fn)" nil nil)
+Display hint for locating error." nil nil)
(autoload 'pg-hint "pg-user" "\
Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil.
@@ -503,14 +655,10 @@ The function `substitute-command-keys' is called on the
argument.
(autoload 'pg-identifier-near-point-query "pg-user" "\
Query the prover about the identifier near point.
If the result is successful, we add a span to the buffer which has
-a popup with the information in it.
-
-\(fn)" t nil)
+a popup with the information in it." t nil)
(autoload 'proof-imenu-enable "pg-user" "\
-Add or remove index menu.
-
-\(fn)" nil nil)
+Add or remove index menu." nil nil)
(autoload 'pg-previous-matching-input-from-input "pg-user" "\
Search backwards through input history for match for current input.
@@ -542,19 +690,25 @@ removed if it matches the last item in the ring.
\(fn CMD)" nil nil)
-(autoload 'pg-clear-input-ring "pg-user" "\
-
-
-\(fn)" nil nil)
+(autoload 'pg-clear-input-ring "pg-user" nil nil nil)
(autoload 'proof-autosend-enable "pg-user" "\
Enable or disable autosend behaviour.
\(fn &optional NOMSG)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-user" '("next-undo-elt" "pg-" "proof-")))
+
;;;***
-;;;### (autoloads nil "pg-xml" "pg-xml.el" (24208 57600 783957 8000))
+;;;### (autoloads nil "pg-vars" "pg-vars.el" (0 0 0 0))
+;;; Generated autoloads from pg-vars.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-vars" '("pg-" "proof-")))
+
+;;;***
+
+;;;### (autoloads nil "pg-xml" "pg-xml.el" (0 0 0 0))
;;; Generated autoloads from pg-xml.el
(autoload 'pg-xml-parse-string "pg-xml" "\
@@ -562,10 +716,26 @@ Parse string in ARG, same as pg-xml-parse-buffer.
\(fn ARG)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"pg-xml" '("pg-")))
+
;;;***
-;;;### (autoloads nil "proof-depends" "proof-depends.el" (24230 6619
-;;;;;; 211624 483000))
+;;;### (autoloads nil "proof-auxmodes" "proof-auxmodes.el" (0 0 0
+;;;;;; 0))
+;;; Generated autoloads from proof-auxmodes.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-auxmodes" '("proof-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-config" "proof-config.el" (0 0 0 0))
+;;; Generated autoloads from proof-config.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-config" '("pbp-" "pg-" "proof-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-depends" "proof-depends.el" (0 0 0 0))
;;; Generated autoloads from proof-depends.el
(autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -582,10 +752,12 @@ specific entries.
\(fn SPAN)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-depends" '("pg-" "proof-")))
+
;;;***
;;;### (autoloads nil "proof-easy-config" "proof-easy-config.el"
-;;;;;; (24208 57600 783957 8000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from proof-easy-config.el
(autoload 'proof-easy-config "proof-easy-config" "\
@@ -596,21 +768,29 @@ Additional arguments are taken into account as a setq
BODY.
\(fn SYM NAME &rest BODY)" nil t)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-easy-config" '("proof-easy-config-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-faces" "proof-faces.el" (0 0 0 0))
+;;; Generated autoloads from proof-faces.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-faces" '("pg-defface-window-systems" "proof-")))
+
;;;***
-;;;### (autoloads nil "proof-indent" "proof-indent.el" (24208 57600
-;;;;;; 783957 8000))
+;;;### (autoloads nil "proof-indent" "proof-indent.el" (0 0 0 0))
;;; Generated autoloads from proof-indent.el
(autoload 'proof-indent-line "proof-indent" "\
-Indent current line of proof script, if indentation enabled.
+Indent current line of proof script, if indentation enabled." t nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-indent" '("proof-indent-")))
;;;***
-;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (24208
-;;;;;; 57600 783957 8000))
+;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (0
+;;;;;; 0 0 0))
;;; Generated autoloads from proof-maths-menu.el
(autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -624,14 +804,11 @@ Turn on or off maths-menu mode in Proof General script
buffer.
This invokes `maths-menu-mode' to toggle the setting for the current
buffer, and then sets PG's option for default to match.
Also we arrange to have maths menu mode turn itself on automatically
-in future if we have just activated it for this buffer.
-
-\(fn)" t nil)
+in future if we have just activated it for this buffer." t nil)
;;;***
-;;;### (autoloads nil "proof-menu" "proof-menu.el" (24631 53911 652410
-;;;;;; 737000))
+;;;### (autoloads nil "proof-menu" "proof-menu.el" (0 0 0 0))
;;; Generated autoloads from proof-menu.el
(autoload 'proof-menu-define-keys "proof-menu" "\
@@ -639,25 +816,18 @@ Prover specific keymap under C-c C-a.
\(fn MAP)" nil nil)
-(autoload 'proof-menu-define-main "proof-menu" "\
+(autoload 'proof-menu-define-main "proof-menu" nil nil nil)
-
-\(fn)" nil nil)
-
-(autoload 'proof-menu-define-specific "proof-menu" "\
-
-
-\(fn)" nil nil)
+(autoload 'proof-menu-define-specific "proof-menu" nil nil nil)
(autoload 'proof-aux-menu "proof-menu" "\
-Construct and return PG auxiliary menu used in non-scripting buffers.
+Construct and return PG auxiliary menu used in non-scripting buffers." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-menu" '("proof-")))
;;;***
-;;;### (autoloads nil "proof-script" "proof-script.el" (24631 49612
-;;;;;; 448031 792000))
+;;;### (autoloads nil "proof-script" "proof-script.el" (0 0 0 0))
;;; Generated autoloads from proof-script.el
(autoload 'proof-ready-for-assistant "proof-script" "\
@@ -667,26 +837,18 @@ If ASSISTANT-NAME is omitted, look up in
`proof-assistant-table'.
\(fn ASSISTANTSYM &optional ASSISTANT-NAME)" nil nil)
(autoload 'proof-colour-locked "proof-script" "\
-Alter the colour of all locked regions according to variable
`proof-colour-locked'.
-
-\(fn)" t nil)
+Alter the colour of all locked regions according to variable
`proof-colour-locked'." t nil)
(autoload 'proof-unprocessed-begin "proof-script" "\
Return end of locked region in current buffer or (point-min) otherwise.
-The position is actually one beyond the last locked character.
-
-\(fn)" nil nil)
+The position is actually one beyond the last locked character." nil nil)
(autoload 'proof-locked-region-full-p "proof-script" "\
Non-nil if the locked region covers all the buffer's non-whitespace.
-Works on any buffer.
-
-\(fn)" nil nil)
+Works on any buffer." nil nil)
(autoload 'proof-locked-region-empty-p "proof-script" "\
-Non-nil if the locked region is empty. Works on any buffer.
-
-\(fn)" nil nil)
+Non-nil if the locked region is empty. Works on any buffer." nil nil)
(autoload 'proof-register-possibly-new-processed-file "proof-script" "\
Register a possibly new FILE as having been processed by the prover.
@@ -713,14 +875,13 @@ Proof General major mode class for proof scripts.
(autoload 'proof-config-done "proof-script" "\
Finish setup of Proof General scripting mode.
Call this function in the derived mode for the proof assistant to
-finish setup which depends on specific proof assistant configuration.
+finish setup which depends on specific proof assistant configuration." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-script" '("pg-" "proof-")))
;;;***
-;;;### (autoloads nil "proof-shell" "proof-shell.el" (24631 49612
-;;;;;; 448031 792000))
+;;;### (autoloads nil "proof-shell" "proof-shell.el" (0 0 0 0))
;;; Generated autoloads from proof-shell.el
(autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -733,15 +894,11 @@ No change to current buffer or point.
\(fn &optional QUEUEMODE)" nil nil)
(autoload 'proof-shell-live-buffer "proof-shell" "\
-Return non-nil if ‘proof-shell-buffer’ is live.
-
-\(fn)" nil nil)
+Return non-nil if ‘proof-shell-buffer’ is live." nil nil)
(autoload 'proof-shell-available-p "proof-shell" "\
Return non-nil if there is a proof shell active and available.
-No error messages. Useful as menu or toolbar enabler.
-
-\(fn)" nil nil)
+No error messages. Useful as menu or toolbar enabler." nil nil)
(autoload 'proof-shell-insert "proof-shell" "\
Insert STRINGS at the end of the proof shell, call `scomint-send-input'.
@@ -849,14 +1006,20 @@ Proof General shell mode class for proof assistant
processes
(autoload 'proof-shell-config-done "proof-shell" "\
Initialise the specific prover after the child has been configured.
Every derived shell mode should call this function at the end of
-processing.
+processing." nil nil)
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-shell" '("pg-" "proof-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-site" "proof-site.el" (0 0 0 0))
+;;; Generated autoloads from proof-site.el
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-site" '("proof")))
;;;***
-;;;### (autoloads nil "proof-splash" "proof-splash.el" (24208 57600
-;;;;;; 783957 8000))
+;;;### (autoloads nil "proof-splash" "proof-splash.el" (0 0 0 0))
;;; Generated autoloads from proof-splash.el
(autoload 'proof-splash-display-screen "proof-splash" "\
@@ -868,14 +1031,13 @@ binding to remove this buffer.
\(fn &optional TIMEOUT)" t nil)
(autoload 'proof-splash-message "proof-splash" "\
-Make sure the user gets welcomed one way or another.
+Make sure the user gets welcomed one way or another." t nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-splash" '("pg-about" "proof-")))
;;;***
-;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (24208 57600
-;;;;;; 783957 8000))
+;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (0 0 0 0))
;;; Generated autoloads from proof-syntax.el
(autoload 'proof-replace-regexp-in-string "proof-syntax" "\
@@ -890,35 +1052,39 @@ may be a string or sexp evaluated to get a string.
\(fn ALIST STRING)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-syntax" '("proof-")))
+
;;;***
-;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (24208 57600
-;;;;;; 783957 8000))
+;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (0 0 0 0))
;;; Generated autoloads from proof-toolbar.el
(autoload 'proof-toolbar-setup "proof-toolbar" "\
Initialize Proof General toolbar and enable it for all PG buffers.
If `proof-toolbar-enable' is nil, change the buffer toolbars
-back the default toolbar.
-
-\(fn)" t nil)
+back the default toolbar." t nil)
(autoload 'proof-toolbar-toggle "proof-toolbar")
(autoload 'proof-toolbar-scripting-menu "proof-toolbar" "\
-Menu made from the Proof General toolbar commands.
+Menu made from the Proof General toolbar commands." nil nil)
-\(fn)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-toolbar" '("proof-toolbar-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-tree" "proof-tree.el" (0 0 0 0))
+;;; Generated autoloads from proof-tree.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-tree" '("proof-tree-")))
;;;***
;;;### (autoloads nil "proof-unicode-tokens" "proof-unicode-tokens.el"
-;;;;;; (24631 49612 448031 792000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from proof-unicode-tokens.el
(autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\
-Turn on or off the Unicode Tokens minor mode in this buffer.
-
-\(fn)" nil nil)
+Turn on or off the Unicode Tokens minor mode in this buffer." nil nil)
(autoload 'proof-unicode-tokens-set-global "proof-unicode-tokens" "\
Set global status of unicode tokens mode for PG buffers to be FLAG.
@@ -933,20 +1099,25 @@ buffer, and then sets PG's option for default to match.
Also we arrange to have unicode tokens mode turn itself on automatically
in future if we have just activated it for this buffer.
Note: this function is called when the customize setting for the prover
-is changed.
+is changed." t nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-unicode-tokens" '("proof-unicode-tokens-")))
;;;***
-;;;### (autoloads nil "proof-utils" "proof-utils.el" (24631 64200
-;;;;;; 229975 917000))
+;;;### (autoloads nil "proof-useropts" "proof-useropts.el" (0 0 0
+;;;;;; 0))
+;;; Generated autoloads from proof-useropts.el
+
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-useropts" '("pg-" "proof-")))
+
+;;;***
+
+;;;### (autoloads nil "proof-utils" "proof-utils.el" (0 0 0 0))
;;; Generated autoloads from proof-utils.el
(autoload 'proof-upgrade-elpa-packages "proof-utils" "\
-Upgrade all ELPA packages (using package.el).
-
-\(fn)" t nil)
+Upgrade all ELPA packages (using package.el)." t nil)
(autoload 'proof-debug "proof-utils" "\
Issue the debugging message (format MSG ARGS) in the *PG Debug* buffer.
@@ -954,10 +1125,12 @@ If flag `proof-general-debug' is nil, do nothing.
\(fn MSG &rest ARGS)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"proof-utils" '("pg-" "proof-")))
+
;;;***
-;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (24208
-;;;;;; 57600 787956 998000))
+;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (0 0 0
+;;;;;; 0))
;;; Generated autoloads from ../lib/scomint.el
(autoload 'scomint-make-in-buffer "../lib/scomint" "\
@@ -986,10 +1159,12 @@ If PROGRAM is a string, the remaining SWITCHES are
arguments to PROGRAM.
\(fn NAME PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/scomint" '("scomint-")))
+
;;;***
;;;### (autoloads nil "../lib/texi-docstring-magic"
"../lib/texi-docstring-magic.el"
-;;;;;; (24631 49612 448031 792000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from ../lib/texi-docstring-magic.el
(autoload 'texi-docstring-magic "../lib/texi-docstring-magic" "\
@@ -999,23 +1174,25 @@ With prefix arg, no errors on unknown symbols. (This
results in
\(fn &optional NOERROR)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/texi-docstring-magic" '("texi-docstring-")))
+
;;;***
;;;### (autoloads nil "../lib/unicode-chars" "../lib/unicode-chars.el"
-;;;;;; (24208 57600 791956 991000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from ../lib/unicode-chars.el
(autoload 'unicode-chars-list-chars "../lib/unicode-chars" "\
Insert each Unicode character into a buffer.
Lets you see which characters are available for literal display
-in your Emacs font.
+in your Emacs font." t nil)
-\(fn)" t nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/unicode-chars" '("unicode-chars-alist")))
;;;***
;;;### (autoloads nil "../lib/unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;; (24208 57600 791956 991000))
+;;;;;; (0 0 0 0))
;;; Generated autoloads from ../lib/unicode-tokens.el
(autoload 'unicode-tokens-encode-str "../lib/unicode-tokens" "\
@@ -1023,18 +1200,12 @@ Return a unicode encoded version presentation of STR.
\(fn STR)" nil nil)
+(if (fboundp 'register-definition-prefixes) (register-definition-prefixes
"../lib/unicode-tokens" '("unicode-tokens-")))
+
;;;***
-;;;### (autoloads nil nil ("../coq/coq-abbrev.el"
"../coq/coq-compile-common.el"
-;;;;;; "../coq/coq-db.el" "../coq/coq-diffs.el" "../coq/coq-indent.el"
-;;;;;; "../coq/coq-local-vars.el" "../coq/coq-par-compile.el"
"../coq/coq-par-test.el"
-;;;;;; "../coq/coq-seq-compile.el" "../coq/coq-smie.el" "../coq/coq-syntax.el"
-;;;;;; "../coq/coq-system.el" "../coq/coq-unicode-tokens.el"
"../lib/local-vars-list.el"
-;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
-;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
-;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-site.el"
-;;;;;; "proof-tree.el" "proof-useropts.el" "proof.el") (24631 50949
-;;;;;; 251401 294000))
+;;;### (autoloads nil nil ("../qrhl/qrhl-input.el" "proof.el") (0
+;;;;;; 0 0 0))
;;;***
diff --git a/generic/proof-site.el b/generic/proof-site.el
index cfaa721958..85819882e3 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -47,6 +47,7 @@
(coq "Coq" "v" nil (".vo" ".glob"))
(easycrypt "EasyCrypt" "ec" "\\.eca?\\'")
(phox "PhoX" "phx" nil (".phi" ".pho"))
+ (qrhl "qRHL" "qrhl")
;; Cut-and-paste management only
diff --git a/qrhl/qrhl-input-25.el b/qrhl/qrhl-input-25.el
new file mode 100644
index 0000000000..6d9fb574ac
--- /dev/null
+++ b/qrhl/qrhl-input-25.el
@@ -0,0 +1,753 @@
+;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in
ProofGeneral -*- lexical-binding: t -*-
+
+;; Copyright (C) 2001-2017 Free Software Foundation, Inc.
+;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009,
+;; 2010, 2011
+;; National Institute of Advanced Industrial Science and Technology (AIST)
+;; Registration Number H14PRO021
+;; Copyright (C) 2017-2022 University of Tartu
+
+;; Author: TAKAHASHI Naoto <ntakahas@m17n.org>
+;; Dave Love <fx@gnu.org>
+;; Dominique Unruh <unruh@ut.ee>
+
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+
+;; Modified by Dominique Unruh to adapt to the specific requirements of
qrhl-tool (https://dominique-unruh.github.io/qrhl-tool/).
+;; Based on latin-ltx.el from Emacs 25.3
(https://git.savannah.gnu.org/cgit/emacs.git/tree/lisp/leim/quail/latin-ltx.el?h=emacs-25.3)
+;; Main changes:
+;; - Added version check (to fail with emacs <26)
+;; - Changed input method name to "qrhl"
+;; - Changed prefix from latin-ltx to qrhl-input
+;; - Changed unicode symbol for \cdot, \llbracket, \rrbracket
+;; - Disabled sequences starting with _
+;; - Appended extra input sequences in the end
+;; - Changed to lexical binding
+
+;; This version is for Emacs 25 since 'qrhl-input.el' is incompatible with
Emacs 25.
+
+;;; Code:
+
+(if (not (version< emacs-version "26"))
+ (error "Emacs version <= 25 required"))
+
+(require 'quail)
+
+(quail-define-package
+ "qrhl" "UTF-8" "\\q " t
+ "LaTeX-like input method for use in the qrhl-tool."
+
+ '(("\t" . quail-completion))
+ t t nil nil nil nil nil nil nil t)
+
+(eval-when-compile
+ (require 'cl-lib)
+
+ (defconst qrhl-input--mark-map
+ '(("DOT BELOW" . "d")
+ ("DOT ABOVE" . ".")
+ ("OGONEK" . "k")
+ ("CEDILLA" . "c")
+ ("CARON" . "v")
+ ;; ("HOOK ABOVE" . ??)
+ ("MACRON" . "=")
+ ("BREVE" . "u")
+ ("TILDE" . "~")
+ ("GRAVE" . "`")
+ ("CIRCUMFLEX" . "^")
+ ("DIAERESIS" . "\"")
+ ("DOUBLE ACUTE" . "H")
+ ("ACUTE" . "'")))
+
+ (defconst qrhl-input--mark-re (regexp-opt (mapcar #'car
qrhl-input--mark-map)))
+
+ (defun qrhl-input--ascii-p (char)
+ (and (characterp char) (< char 128)))
+
+ (defmacro qrhl-input--define-rules (&rest rules)
+ (load "uni-name")
+ (let ((newrules ()))
+ (dolist (rule rules)
+ (pcase rule
+ (`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule.
+ (`(,seq ,re)
+ (let ((count 0)
+ (re (eval re t)))
+ (dolist (pair (ucs-names))
+ (let ((name (car pair))
+ (char (cdr pair)))
+ (when (and (characterp char) ;; Ignore char-ranges.
+ (string-match re name))
+ (let ((keys (if (stringp seq)
+ (replace-match seq nil nil name)
+ (funcall seq name char))))
+ (if (listp keys)
+ (dolist (x keys)
+ (setq count (1+ count))
+ (push (list x char) newrules))
+ (setq count (1+ count))
+ (push (list keys char) newrules))))))
+ ;; (message "qrhl-input: %d mappings for %S" count re)
+ ))))
+ (setq newrules (delete-dups newrules))
+ (let ((rules (copy-sequence newrules)))
+ (while rules
+ (let ((rule (pop rules)))
+ (when (assoc (car rule) rules)
+ (let ((conflicts (list (cadr rule)))
+ (tail rules)
+ c)
+ (while (setq c (assoc (car rule) tail))
+ (push (cadr c) conflicts)
+ (setq tail (cdr (memq c tail)))
+ (setq rules (delq c rules)))
+ (message "Conflict for %S: %S"
+ (car rule) (apply #'string conflicts)))))))
+ (let ((inputs (mapcar #'car newrules)))
+ (setq inputs (delete-dups inputs))
+ (message "qrhl-input: %d rules (+ %d conflicts)!"
+ (length inputs) (- (length newrules) (length inputs))))
+ `(quail-define-rules ,@(nreverse newrules)))))
+
+(qrhl-input--define-rules
+ ("!`" ?¡)
+ ("\\pounds" ?£) ;; ("{\\pounds}" ?£)
+ ("\\S" ?§) ;; ("{\\S}" ?§)
+ ("$^a$" ?ª)
+ ("$\\pm$" ?±) ("\\pm" ?±)
+ ("$^2$" ?²)
+ ("$^3$" ?³)
+ ("\\P" ?¶) ;; ("{\\P}" ?¶)
+ ("$\\cdot$" ?⋅) ("\\cdot" ?⋅)
+ ("$^1$" ?¹)
+ ("$^o$" ?º)
+ ("?`" ?¿)
+
+ ((lambda (name char)
+ (let* ((c (if (match-end 1)
+ (downcase (match-string 2 name))
+ (match-string 2 name)))
+ (mark1 (cdr (assoc (match-string 3 name) qrhl-input--mark-map)))
+ (mark2 (if (match-end 4)
+ (cdr (assoc (match-string 4 name)
qrhl-input--mark-map))))
+ (marks (if mark2 (concat mark1 "\\" mark2) mark1)))
+ (cl-assert mark1)
+ (cons (format "\\%s{%s}" marks c)
+ ;; Exclude "d" because we use "\\dh" for something else.
+ (unless (member (or mark2 mark1) '("d"));; "k"
+ (list (format "\\%s%s" marks c))))))
+ (concat "\\`LATIN \\(?:CAPITAL\\|SMAL\\(L\\)\\) LETTER \\(.\\) WITH \\("
+ qrhl-input--mark-re "\\)\\(?: AND \\("
+ qrhl-input--mark-re "\\)\\)?\\'"))
+
+ ((lambda (name char)
+ (let* ((mark (cdr (assoc (match-string 1 name) qrhl-input--mark-map))))
+ (cl-assert mark)
+ (list (format "\\%s" mark))))
+ (concat "\\`COMBINING \\(" qrhl-input--mark-re "\\)\\(?: ACCENT\\)?\\'"))
+
+ ((lambda (name char)
+ (unless (qrhl-input--ascii-p char)
+ (let* ((mark (cdr (assoc (match-string 1 name) qrhl-input--mark-map))))
+ (cl-assert mark)
+ (list (format "\\%s{}" mark)))))
+ (concat "\\`\\(?:SPACING \\)?\\(" qrhl-input--mark-re "\\)\\(?:
ACCENT\\)?\\'"))
+
+ ("\\AA" ?Å) ;; ("{\\AA}" ?Å)
+ ("\\AE" ?Æ) ;; ("{\\AE}" ?Æ)
+
+ ("$\\times$" ?×) ("\\times" ?×)
+ ("\\O" ?Ø) ;; ("{\\O}" ?Ø)
+ ("\\ss" ?ß) ;; ("{\\ss}" ?ß)
+
+ ("\\aa" ?å) ;; ("{\\aa}" ?å)
+ ("\\ae" ?æ) ;; ("{\\ae}" ?æ)
+
+ ("$\\div$" ?÷) ("\\div" ?÷)
+ ("\\o" ?ø) ;; ("{\\o}" ?ø)
+
+ ("\\~{\\i}" ?ĩ)
+ ("\\={\\i}" ?ī)
+ ("\\u{\\i}" ?ĭ)
+
+ ("\\i" ?ı) ;; ("{\\i}" ?ı)
+ ("\\^{\\j}" ?ĵ)
+
+ ("\\L" ?Ł) ;; ("{\\L}" ?Ł)
+ ("\\l" ?ł) ;; ("{\\l}" ?ł)
+
+ ("\\H" ?̋)
+ ("\\H{}" ?˝)
+ ("\\U{o}" ?ő) ("\\Uo" ?ő) ;; FIXME: Was it just a typo?
+
+ ("\\OE" ?Œ) ;; ("{\\OE}" ?Œ)
+ ("\\oe" ?œ) ;; ("{\\oe}" ?œ)
+
+ ("\\v{\\i}" ?ǐ)
+
+ ("\\={\\AE}" ?Ǣ) ("\\=\\AE" ?Ǣ)
+ ("\\={\\ae}" ?ǣ) ("\\=\\ae" ?ǣ)
+
+ ("\\v{\\j}" ?ǰ)
+ ("\\'{\\AE}" ?Ǽ) ("\\'\\AE" ?Ǽ)
+ ("\\'{\\ae}" ?ǽ) ("\\'\\ae" ?ǽ)
+ ("\\'{\\O}" ?Ǿ) ("\\'\\O" ?Ǿ)
+ ("\\'{\\o}" ?ǿ) ("\\'\\o" ?ǿ)
+
+ ("\\," ? )
+ ("\\/" ?)
+ ("\\:" ? )
+ ("\\;" ? )
+
+ ;; ;; Dominique Unruh: Disabling _1 etc.
+ ;; ((lambda (name char)
+ ;; (let* ((base (concat (match-string 1 name) (match-string 3 name)))
+ ;; (basechar (cdr (assoc base (ucs-names)))))
+ ;; (when (qrhl-input--ascii-p basechar)
+ ;; (string (if (match-end 2) ?^ ?_) basechar))))
+ ;; "\\(.*\\)SU\\(?:B\\|\\(PER\\)\\)SCRIPT \\(.*\\)")
+
+ ((lambda (name _char)
+ (let* ((basename (match-string 2 name))
+ (name (if (match-end 1) (capitalize basename) (downcase basename))))
+ (concat "^" (if (> (length name) 1) "\\") name)))
+ "\\`MODIFIER LETTER \\(?:SMALL\\|CAPITA\\(L\\)\\) \\([[:ascii:]]+\\)\\'")
+
+ ;; ((lambda (name char) (format "^%s" (downcase (match-string 1 name))))
+ ;; "\\`MODIFIER LETTER SMALL \\(.\\)\\'")
+ ;; ("^\\1" "\\`MODIFIER LETTER CAPITAL \\(.\\)\\'")
+ ("^o_" ?º)
+ ("^{SM}" ?℠)
+ ("^{TEL}" ?℡)
+ ("^{TM}" ?™)
+
+ ("\\b" ?̱)
+
+ ("\\rq" ?’)
+
+ ;; FIXME: Provides some useful entries (yen, euro, copyright, registered,
+ ;; currency, minus, micro), but also a lot of dubious ones.
+ ((lambda (name char)
+ (unless (or (qrhl-input--ascii-p char)
+ ;; We prefer COMBINING LONG SOLIDUS OVERLAY for \not.
+ (member name '("NOT SIGN")))
+ (concat "\\" (downcase (match-string 1 name)))))
+ "\\`\\([^- ]+\\) SIGN\\'")
+
+ ((lambda (name char)
+ (concat "\\" (funcall (if (match-end 1) #' capitalize #'downcase)
+ (match-string 2 name))))
+ "\\`GREEK \\(?:SMALL\\|CAPITA\\(L\\)\\) LETTER \\([^- ]+\\)\\'")
+
+ ("\\Box" ?□)
+ ("\\Bumpeq" ?≎)
+ ("\\Cap" ?⋒)
+ ("\\Cup" ?⋓)
+ ("\\Diamond" ?◇)
+ ("\\Downarrow" ?⇓)
+ ("\\H{o}" ?ő)
+ ("\\Im" ?ℑ)
+ ("\\Join" ?⋈)
+ ("\\Leftarrow" ?⇐)
+ ("\\Leftrightarrow" ?⇔)
+ ("\\Ll" ?⋘)
+ ("\\Lleftarrow" ?⇚)
+ ("\\Longleftarrow" ?⇐)
+ ("\\Longleftrightarrow" ?⇔)
+ ("\\Longrightarrow" ?⇒)
+ ("\\Lsh" ?↰)
+ ("\\Re" ?ℜ)
+ ("\\Rightarrow" ?⇒)
+ ("\\Rrightarrow" ?⇛)
+ ("\\Rsh" ?↱)
+ ("\\Subset" ?⋐)
+ ("\\Supset" ?⋑)
+ ("\\Uparrow" ?⇑)
+ ("\\Updownarrow" ?⇕)
+ ("\\Vdash" ?⊩)
+ ("\\Vert" ?‖)
+ ("\\Vvdash" ?⊪)
+ ("\\aleph" ?ℵ)
+ ("\\amalg" ?∐)
+ ("\\angle" ?∠)
+ ("\\approx" ?≈)
+ ("\\approxeq" ?≊)
+ ("\\ast" ?∗)
+ ("\\asymp" ?≍)
+ ("\\backcong" ?≌)
+ ("\\backepsilon" ?∍)
+ ("\\backprime" ?‵)
+ ("\\backsim" ?∽)
+ ("\\backsimeq" ?⋍)
+ ("\\backslash" ?\\)
+ ("\\barwedge" ?⊼)
+ ("\\because" ?∵)
+ ("\\beth" ?ℶ)
+ ("\\between" ?≬)
+ ("\\bigcap" ?⋂)
+ ("\\bigcirc" ?◯)
+ ("\\bigcup" ?⋃)
+ ("\\bigstar" ?★)
+ ("\\bigtriangledown" ?▽)
+ ("\\bigtriangleup" ?△)
+ ("\\bigvee" ?⋁)
+ ("\\bigwedge" ?⋀)
+ ("\\blacklozenge" ?✦)
+ ("\\blacksquare" ?▪)
+ ("\\blacktriangle" ?▴)
+ ("\\blacktriangledown" ?▾)
+ ("\\blacktriangleleft" ?◂)
+ ("\\blacktriangleright" ?▸)
+ ("\\bot" ?⊥)
+ ("\\bowtie" ?⋈)
+ ("\\boxminus" ?⊟)
+ ("\\boxplus" ?⊞)
+ ("\\boxtimes" ?⊠)
+ ("\\bullet" ?•)
+ ("\\bumpeq" ?≏)
+ ("\\cap" ?∩)
+ ("\\cdots" ?⋯)
+ ("\\centerdot" ?⋅)
+ ("\\checkmark" ?✓)
+ ("\\chi" ?χ)
+ ("\\circ" ?∘)
+ ("\\circeq" ?≗)
+ ("\\circlearrowleft" ?↺)
+ ("\\circlearrowright" ?↻)
+ ("\\circledR" ?®)
+ ("\\circledS" ?Ⓢ)
+ ("\\circledast" ?⊛)
+ ("\\circledcirc" ?⊚)
+ ("\\circleddash" ?⊝)
+ ("\\clubsuit" ?♣)
+ ("\\coloneq" ?≔)
+ ("\\complement" ?∁)
+ ("\\cong" ?≅)
+ ("\\coprod" ?∐)
+ ("\\cup" ?∪)
+ ("\\curlyeqprec" ?⋞)
+ ("\\curlyeqsucc" ?⋟)
+ ("\\curlypreceq" ?≼)
+ ("\\curlyvee" ?⋎)
+ ("\\curlywedge" ?⋏)
+ ("\\curvearrowleft" ?↶)
+ ("\\curvearrowright" ?↷)
+
+ ("\\dag" ?†)
+ ("\\dagger" ?†)
+ ("\\daleth" ?ℸ)
+ ("\\dashv" ?⊣)
+ ("\\ddag" ?‡)
+ ("\\ddagger" ?‡)
+ ("\\ddots" ?⋱)
+ ("\\diamond" ?⋄)
+ ("\\diamondsuit" ?♢)
+ ("\\divideontimes" ?⋇)
+ ("\\doteq" ?≐)
+ ("\\doteqdot" ?≑)
+ ("\\dotplus" ?∔)
+ ("\\dotsquare" ?⊡)
+ ("\\downarrow" ?↓)
+ ("\\downdownarrows" ?⇊)
+ ("\\downleftharpoon" ?⇃)
+ ("\\downrightharpoon" ?⇂)
+ ("\\ell" ?ℓ)
+ ("\\emptyset" ?∅)
+ ("\\eqcirc" ?≖)
+ ("\\eqcolon" ?≕)
+ ("\\eqslantgtr" ?⋝)
+ ("\\eqslantless" ?⋜)
+ ("\\equiv" ?≡)
+ ("\\exists" ?∃)
+ ("\\fallingdotseq" ?≒)
+ ("\\flat" ?♭)
+ ("\\forall" ?∀)
+ ("\\frac1" ?⅟)
+ ("\\frac12" ?½)
+ ("\\frac13" ?⅓)
+ ("\\frac14" ?¼)
+ ("\\frac15" ?⅕)
+ ("\\frac16" ?⅙)
+ ("\\frac18" ?⅛)
+ ("\\frac23" ?⅔)
+ ("\\frac25" ?⅖)
+ ("\\frac34" ?¾)
+ ("\\frac35" ?⅗)
+ ("\\frac38" ?⅜)
+ ("\\frac45" ?⅘)
+ ("\\frac56" ?⅚)
+ ("\\frac58" ?⅝)
+ ("\\frac78" ?⅞)
+ ("\\frown" ?⌢)
+ ("\\ge" ?≥)
+ ("\\geq" ?≥)
+ ("\\geqq" ?≧)
+ ("\\geqslant" ?≥)
+ ("\\gets" ?←)
+ ("\\gg" ?≫)
+ ("\\ggg" ?⋙)
+ ("\\gimel" ?ℷ)
+ ("\\gnapprox" ?⋧)
+ ("\\gneq" ?≩)
+ ("\\gneqq" ?≩)
+ ("\\gnsim" ?⋧)
+ ("\\gtrapprox" ?≳)
+ ("\\gtrdot" ?⋗)
+ ("\\gtreqless" ?⋛)
+ ("\\gtreqqless" ?⋛)
+ ("\\gtrless" ?≷)
+ ("\\gtrsim" ?≳)
+ ("\\gvertneqq" ?≩)
+ ("\\hbar" ?ℏ)
+ ("\\heartsuit" ?♥)
+ ("\\hookleftarrow" ?↩)
+ ("\\hookrightarrow" ?↪)
+ ("\\iff" ?⇔)
+ ("\\imath" ?ı)
+ ("\\in" ?∈)
+ ("\\infty" ?∞)
+ ("\\int" ?∫)
+ ("\\intercal" ?⊺)
+ ("\\langle" ?⟨) ;; Was ?〈, see bug#12948.
+ ("\\lbrace" ?{)
+ ("\\lbrack" ?\[)
+ ("\\lceil" ?⌈)
+ ("\\ldots" ?…)
+ ("\\le" ?≤)
+ ("\\leadsto" ?↝)
+ ("\\leftarrow" ?←)
+ ("\\leftarrowtail" ?↢)
+ ("\\leftharpoondown" ?↽)
+ ("\\leftharpoonup" ?↼)
+ ("\\leftleftarrows" ?⇇)
+ ;; ("\\leftparengtr" ?〈), see bug#12948.
+ ("\\leftrightarrow" ?↔)
+ ("\\leftrightarrows" ?⇆)
+ ("\\leftrightharpoons" ?⇋)
+ ("\\leftrightsquigarrow" ?↭)
+ ("\\leftthreetimes" ?⋋)
+ ("\\leq" ?≤)
+ ("\\leqq" ?≦)
+ ("\\leqslant" ?≤)
+ ("\\lessapprox" ?≲)
+ ("\\lessdot" ?⋖)
+ ("\\lesseqgtr" ?⋚)
+ ("\\lesseqqgtr" ?⋚)
+ ("\\lessgtr" ?≶)
+ ("\\lesssim" ?≲)
+ ("\\lfloor" ?⌊)
+ ("\\lhd" ?◁)
+ ("\\rhd" ?▷)
+ ("\\ll" ?≪)
+ ("\\llcorner" ?⌞)
+ ("\\lnapprox" ?⋦)
+ ("\\lneq" ?≨)
+ ("\\lneqq" ?≨)
+ ("\\lnsim" ?⋦)
+ ("\\longleftarrow" ?←)
+ ("\\longleftrightarrow" ?↔)
+ ("\\longmapsto" ?↦)
+ ("\\longrightarrow" ?→)
+ ("\\looparrowleft" ?↫)
+ ("\\looparrowright" ?↬)
+ ("\\lozenge" ?✧)
+ ("\\lq" ?‘)
+ ("\\lrcorner" ?⌟)
+ ("\\ltimes" ?⋉)
+ ("\\lvertneqq" ?≨)
+ ("\\maltese" ?✠)
+ ("\\mapsto" ?↦)
+ ("\\measuredangle" ?∡)
+ ("\\mho" ?℧)
+ ("\\mid" ?∣)
+ ("\\models" ?⊧)
+ ("\\mp" ?∓)
+ ("\\multimap" ?⊸)
+ ("\\nLeftarrow" ?⇍)
+ ("\\nLeftrightarrow" ?⇎)
+ ("\\nRightarrow" ?⇏)
+ ("\\nVDash" ?⊯)
+ ("\\nVdash" ?⊮)
+ ("\\nabla" ?∇)
+ ("\\napprox" ?≉)
+ ("\\natural" ?♮)
+ ("\\ncong" ?≇)
+ ("\\ne" ?≠)
+ ("\\nearrow" ?↗)
+ ("\\neg" ?¬)
+ ("\\neq" ?≠)
+ ("\\nequiv" ?≢)
+ ("\\newline" ?
)
+ ("\\nexists" ?∄)
+ ("\\ngeq" ?≱)
+ ("\\ngeqq" ?≱)
+ ("\\ngeqslant" ?≱)
+ ("\\ngtr" ?≯)
+ ("\\ni" ?∋)
+ ("\\nleftarrow" ?↚)
+ ("\\nleftrightarrow" ?↮)
+ ("\\nleq" ?≰)
+ ("\\nleqq" ?≰)
+ ("\\nleqslant" ?≰)
+ ("\\nless" ?≮)
+ ("\\nmid" ?∤)
+ ("\\not" ?̸) ;FIXME: conflict with "NOT SIGN" ¬.
+ ("\\notin" ?∉)
+ ("\\nparallel" ?∦)
+ ("\\nprec" ?⊀)
+ ("\\npreceq" ?⋠)
+ ("\\nrightarrow" ?↛)
+ ("\\nshortmid" ?∤)
+ ("\\nshortparallel" ?∦)
+ ("\\nsim" ?≁)
+ ("\\nsimeq" ?≄)
+ ("\\nsubset" ?⊄)
+ ("\\nsubseteq" ?⊈)
+ ("\\nsubseteqq" ?⊈)
+ ("\\nsucc" ?⊁)
+ ("\\nsucceq" ?⋡)
+ ("\\nsupset" ?⊅)
+ ("\\nsupseteq" ?⊉)
+ ("\\nsupseteqq" ?⊉)
+ ("\\ntriangleleft" ?⋪)
+ ("\\ntrianglelefteq" ?⋬)
+ ("\\ntriangleright" ?⋫)
+ ("\\ntrianglerighteq" ?⋭)
+ ("\\nvDash" ?⊭)
+ ("\\nvdash" ?⊬)
+ ("\\nwarrow" ?↖)
+ ("\\odot" ?⊙)
+ ("\\oint" ?∮)
+ ("\\ominus" ?⊖)
+ ("\\oplus" ?⊕)
+ ("\\oslash" ?⊘)
+ ("\\otimes" ?⊗)
+ ("\\par" ?
)
+ ("\\parallel" ?∥)
+ ("\\partial" ?∂)
+ ("\\perp" ?⊥)
+ ("\\pitchfork" ?⋔)
+ ("\\prec" ?≺)
+ ("\\precapprox" ?≾)
+ ("\\preceq" ?≼)
+ ("\\precnapprox" ?⋨)
+ ("\\precnsim" ?⋨)
+ ("\\precsim" ?≾)
+ ("\\prime" ?′)
+ ("\\prod" ?∏)
+ ("\\propto" ?∝)
+ ("\\qed" ?∎)
+ ("\\quad" ? )
+ ("\\rangle" ?⟩) ;; Was ?〉, see bug#12948.
+ ("\\rbrace" ?})
+ ("\\rbrack" ?\])
+ ("\\rceil" ?⌉)
+ ("\\rfloor" ?⌋)
+ ("\\rightarrow" ?→)
+ ("\\rightarrowtail" ?↣)
+ ("\\rightharpoondown" ?⇁)
+ ("\\rightharpoonup" ?⇀)
+ ("\\rightleftarrows" ?⇄)
+ ("\\rightleftharpoons" ?⇌)
+ ;; ("\\rightparengtr" ?⦔) ;; Was ?〉, see bug#12948.
+ ("\\rightrightarrows" ?⇉)
+ ("\\rightthreetimes" ?⋌)
+ ("\\risingdotseq" ?≓)
+ ("\\rtimes" ?⋊)
+ ("\\sbs" ?﹨)
+ ("\\searrow" ?↘)
+ ("\\setminus" ?∖)
+ ("\\sharp" ?♯)
+ ("\\shortmid" ?∣)
+ ("\\shortparallel" ?∥)
+ ("\\sim" ?∼)
+ ("\\simeq" ?≃)
+ ("\\smallamalg" ?∐)
+ ("\\smallsetminus" ?∖)
+ ("\\smallsmile" ?⌣)
+ ("\\smile" ?⌣)
+ ("\\spadesuit" ?♠)
+ ("\\sphericalangle" ?∢)
+ ("\\sqcap" ?⊓)
+ ("\\sqcup" ?⊔)
+ ("\\sqsubset" ?⊏)
+ ("\\sqsubseteq" ?⊑)
+ ("\\sqsupset" ?⊐)
+ ("\\sqsupseteq" ?⊒)
+ ("\\square" ?□)
+ ("\\squigarrowright" ?⇝)
+ ("\\star" ?⋆)
+ ("\\straightphi" ?φ)
+ ("\\subset" ?⊂)
+ ("\\subseteq" ?⊆)
+ ("\\subseteqq" ?⊆)
+ ("\\subsetneq" ?⊊)
+ ("\\subsetneqq" ?⊊)
+ ("\\succ" ?≻)
+ ("\\succapprox" ?≿)
+ ("\\succcurlyeq" ?≽)
+ ("\\succeq" ?≽)
+ ("\\succnapprox" ?⋩)
+ ("\\succnsim" ?⋩)
+ ("\\succsim" ?≿)
+ ("\\sum" ?∑)
+ ("\\supset" ?⊃)
+ ("\\supseteq" ?⊇)
+ ("\\supseteqq" ?⊇)
+ ("\\supsetneq" ?⊋)
+ ("\\supsetneqq" ?⊋)
+ ("\\surd" ?√)
+ ("\\swarrow" ?↙)
+ ("\\therefore" ?∴)
+ ("\\thickapprox" ?≈)
+ ("\\thicksim" ?∼)
+ ("\\to" ?→)
+ ("\\top" ?⊤)
+ ("\\triangle" ?▵)
+ ("\\triangledown" ?▿)
+ ("\\triangleleft" ?◃)
+ ("\\trianglelefteq" ?⊴)
+ ("\\triangleq" ?≜)
+ ("\\triangleright" ?▹)
+ ("\\trianglerighteq" ?⊵)
+ ("\\twoheadleftarrow" ?↞)
+ ("\\twoheadrightarrow" ?↠)
+ ("\\ulcorner" ?⌜)
+ ("\\uparrow" ?↑)
+ ("\\updownarrow" ?↕)
+ ("\\upleftharpoon" ?↿)
+ ("\\uplus" ?⊎)
+ ("\\uprightharpoon" ?↾)
+ ("\\upuparrows" ?⇈)
+ ("\\urcorner" ?⌝)
+ ("\\u{i}" ?ĭ)
+ ("\\vDash" ?⊨)
+
+ ((lambda (name char)
+ (concat "\\var" (downcase (match-string 1 name))))
+ "\\`GREEK \\([^- ]+\\) SYMBOL\\'")
+
+ ("\\varprime" ?′)
+ ("\\varpropto" ?∝)
+ ("\\varsigma" ?ς) ;FIXME: Looks reversed with the non\var.
+ ("\\vartriangleleft" ?⊲)
+ ("\\vartriangleright" ?⊳)
+ ("\\vdash" ?⊢)
+ ("\\vdots" ?⋮)
+ ("\\vee" ?∨)
+ ("\\veebar" ?⊻)
+ ("\\vert" ?|)
+ ("\\wedge" ?∧)
+ ("\\wp" ?℘)
+ ("\\wr" ?≀)
+
+ ("\\Bbb{N}" ?ℕ) ; AMS commands for blackboard bold
+ ("\\Bbb{P}" ?ℙ) ; Also sometimes \mathbb.
+ ("\\Bbb{R}" ?ℝ)
+ ("\\Bbb{Z}" ?ℤ)
+ ("--" ?–)
+ ("---" ?—)
+ ;; We used to use ~ for NBSP but that's inconvenient and may even look like
+ ;; a bug where the user finds his ~ key doesn't insert a ~ any more.
+ ("\\ " ? )
+ ("\\\\" ?\\)
+ ("\\mathscr{I}" ?ℐ) ; moment of inertia
+ ("\\Smiley" ?☺)
+ ("\\blacksmiley" ?☻)
+ ("\\Frowny" ?☹)
+ ("\\Letter" ?✉)
+ ("\\permil" ?‰)
+ ;; Probably not useful enough:
+ ;; ("\\Telefon" ?☎) ; there are other possibilities
+ ;; ("\\Radioactivity" ?☢)
+ ;; ("\\Biohazard" ?☣)
+ ;; ("\\Male" ?♂)
+ ;; ("\\Female" ?♀)
+ ;; ("\\Lightning" ?☇)
+ ;; ("\\Mercury" ?☿)
+ ;; ("\\Earth" ?♁)
+ ;; ("\\Jupiter" ?♃)
+ ;; ("\\Saturn" ?♄)
+ ;; ("\\Uranus" ?♅)
+ ;; ("\\Neptune" ?♆)
+ ;; ("\\Pluto" ?♇)
+ ;; ("\\Sun" ?☉)
+ ;; ("\\Writinghand" ?✍)
+ ;; ("\\Yinyang" ?☯)
+ ;; ("\\Heart" ?♡)
+ ("\\dh" ?ð)
+ ("\\DH" ?Ð)
+ ("\\th" ?þ)
+ ("\\TH" ?Þ)
+ ("\\lnot" ?¬)
+ ("\\ordfeminine" ?ª)
+ ("\\ordmasculine" ?º)
+ ("\\lambdabar" ?ƛ)
+ ("\\celsius" ?℃)
+ ;; by analogy with lq, rq:
+ ("\\ldq" ?\“)
+ ("\\rdq" ?\”)
+ ("\\defs" ?≙) ; per fuzz/zed
+ ;; ("\\sqrt[3]" ?∛)
+ ("\\llbracket" ?\⟦) ; stmaryrd
+ ("\\rrbracket" ?\⟧)
+ ;; ("\\lbag" ?\〚) ; fuzz
+ ;; ("\\rbag" ?\〛)
+ ("\\ldata" ?\《) ; fuzz/zed
+ ("\\rdata" ?\》)
+ ;; From Karl Eichwalder.
+ ("\\glq" ?‚)
+ ("\\grq" ?‘)
+ ("\\glqq" ?„) ("\\\"`" ?„)
+ ("\\grqq" ?“) ("\\\"'" ?“)
+ ("\\flq" ?‹)
+ ("\\frq" ?›)
+ ("\\flqq" ?\«) ("\\\"<" ?\«)
+ ("\\frqq" ?\») ("\\\">" ?\»)
+
+ ("\\-" ?) ;; soft hyphen
+
+ ("\\textmu" ?µ)
+ ("\\textfractionsolidus" ?⁄)
+ ("\\textbigcircle" ?⃝)
+ ("\\textmusicalnote" ?♪)
+ ("\\textdied" ?✝)
+ ("\\textcolonmonetary" ?₡)
+ ("\\textwon" ?₩)
+ ("\\textnaira" ?₦)
+ ("\\textpeso" ?₱)
+ ("\\textlira" ?₤)
+ ("\\textrecipe" ?℞)
+ ("\\textinterrobang" ?‽)
+ ("\\textpertenthousand" ?‱)
+ ("\\textbaht" ?฿)
+ ("\\textnumero" ?№)
+ ("\\textdiscount" ?⁒)
+ ("\\textestimated" ?℮)
+ ("\\textopenbullet" ?◦)
+ ("\\textlquill" ?⁅)
+ ("\\textrquill" ?⁆)
+ ("\\textcircledP" ?℗)
+ ("\\textreferencemark" ?※)
+ )
+
+
+;; Dominique's rules for qrhl-tool:
+(quail-define-rules
+ ((append . t))
+ ("\\ox" ?⊗)
+ ("\\ket" ["|⟩"])
+ ("\\ket0" ["|0⟩"])
+ ("\\ket1" ["|1⟩"])
+ ("[|" ["⟦"])
+ ("|]" ["⟧"])
+ (">>" ?»)
+ ("\\Cla" ["ℭ𝔩𝔞"])
+ ("\\qeq" ["≡𝔮"])
+ )
+
+(provide 'qrhl-input-25)
+
+;;; qrhl-input.el ends here
diff --git a/qrhl/qrhl-input.el b/qrhl/qrhl-input.el
new file mode 100644
index 0000000000..8cc520425c
--- /dev/null
+++ b/qrhl/qrhl-input.el
@@ -0,0 +1,763 @@
+;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in
ProofGeneral -*-coding: utf-8;-*-
+
+;; Copyright (C) 2001-2018 Free Software Foundation, Inc.
+;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009,
+;; 2010, 2011
+;; National Institute of Advanced Industrial Science and Technology (AIST)
+;; Registration Number H14PRO021
+;; Copyright (C) 2017-2022 University of Tartu
+
+;; Author: TAKAHASHI Naoto <ntakahas@m17n.org>
+;; Dave Love <fx@gnu.org>
+;; Dominique Unruh <unruh@ut.ee>
+
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+
+;; Modified by Dominique Unruh to adapt to the specific requirements of
qrhl-tool (https://dominique-unruh.github.io/qrhl-tool/).
+;; Based on latin-ltx.el from Emacs 26.3
(https://git.savannah.gnu.org/cgit/emacs.git/tree/lisp/leim/quail/latin-ltx.el?h=emacs-26.3)
+;; Main changes:
+;; - Added version check (to fail with emacs <26)
+;; - Changed input method name to "qrhl"
+;; - Changed prefix from latin-ltx to qrhl-input
+;; - Changed unicode symbol for \cdot, \llbracket, \rrbracket
+;; - Disabled sequences starting with _
+;; - Appended extra input sequences in the end
+;; - Changed to lexical binding
+
+;;; Code:
+
+(if (version< emacs-version "26")
+ (error "Emacs version >= 26 required"))
+
+(require 'quail)
+
+(quail-define-package
+ "qrhl" "UTF-8" "\\q " t
+ "LaTeX-like input method for use in the qrhl-tool."
+
+ '(("\t" . quail-completion))
+ t t nil nil nil nil nil nil nil t)
+
+(eval-when-compile
+ (require 'cl-lib)
+
+ (defconst qrhl-input--mark-map
+ '(("DOT BELOW" . "d")
+ ("DOT ABOVE" . ".")
+ ("OGONEK" . "k")
+ ("CEDILLA" . "c")
+ ("CARON" . "v")
+ ;; ("HOOK ABOVE" . ??)
+ ("MACRON" . "=")
+ ("BREVE" . "u")
+ ("TILDE" . "~")
+ ("GRAVE" . "`")
+ ("CIRCUMFLEX" . "^")
+ ("DIAERESIS" . "\"")
+ ("DOUBLE ACUTE" . "H")
+ ("ACUTE" . "'")))
+
+ (defconst qrhl-input--mark-re (regexp-opt (mapcar #'car
qrhl-input--mark-map)))
+
+ (defun qrhl-input--ascii-p (char)
+ (and (characterp char) (< char 128)))
+
+ (defmacro qrhl-input--define-rules (&rest rules)
+ (load "uni-name")
+ (let ((newrules ()))
+ (dolist (rule rules)
+ (pcase rule
+ (`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule.
+ (`(,seq ,re)
+ (let ((count 0)
+ (re (eval re t)))
+ (maphash
+ (lambda (name char)
+ (when (and (characterp char) ;; Ignore char-ranges.
+ (string-match re name))
+ (let ((keys (if (stringp seq)
+ (replace-match seq nil nil name)
+ (funcall seq name char))))
+ (if (listp keys)
+ (dolist (x keys)
+ (setq count (1+ count))
+ (push (list x char) newrules))
+ (setq count (1+ count))
+ (push (list keys char) newrules)))))
+ (ucs-names))
+ ;; (message "qrhl-input: %d mappings for %S" count re)
+ ))))
+ (setq newrules (delete-dups newrules))
+ (let ((rules (copy-sequence newrules)))
+ (while rules
+ (let ((rule (pop rules)))
+ (when (assoc (car rule) rules)
+ (let ((conflicts (list (cadr rule)))
+ (tail rules)
+ c)
+ (while (setq c (assoc (car rule) tail))
+ (push (cadr c) conflicts)
+ (setq tail (cdr (memq c tail)))
+ (setq rules (delq c rules)))
+ (message "Conflict for %S: %S"
+ (car rule) (apply #'string conflicts)))))))
+ (let ((inputs (mapcar #'car newrules)))
+ (setq inputs (delete-dups inputs))
+ (message "qrhl-input: %d rules (+ %d conflicts)!"
+ (length inputs) (- (length newrules) (length inputs))))
+ `(quail-define-rules ,@(nreverse newrules)))))
+
+(qrhl-input--define-rules
+
+ ("!`" ?¡)
+ ("\\pounds" ?£) ;; ("{\\pounds}" ?£)
+ ("\\S" ?§) ;; ("{\\S}" ?§)
+ ("$^a$" ?ª)
+ ("$\\pm$" ?±) ("\\pm" ?±)
+ ("$^2$" ?²)
+ ("$^3$" ?³)
+ ("\\P" ?¶) ;; ("{\\P}" ?¶)
+ ("$\\cdot$" ?⋅) ("\\cdot" ?⋅)
+ ("$^1$" ?¹)
+ ("$^o$" ?º)
+ ("?`" ?¿)
+
+ ((lambda (name char)
+ (let* ((c (if (match-end 1)
+ (downcase (match-string 2 name))
+ (match-string 2 name)))
+ (mark1 (cdr (assoc (match-string 3 name) qrhl-input--mark-map)))
+ (mark2 (if (match-end 4)
+ (cdr (assoc (match-string 4 name)
qrhl-input--mark-map))))
+ (marks (if mark2 (concat mark1 "\\" mark2) mark1)))
+ (cl-assert mark1)
+ (cons (format "\\%s{%s}" marks c)
+ ;; Exclude "d" because we use "\\dh" for something else.
+ (unless (member (or mark2 mark1) '("d"));; "k"
+ (list (format "\\%s%s" marks c))))))
+ (concat "\\`LATIN \\(?:CAPITAL\\|SMAL\\(L\\)\\) LETTER \\(.\\) WITH \\("
+ qrhl-input--mark-re "\\)\\(?: AND \\("
+ qrhl-input--mark-re "\\)\\)?\\'"))
+
+ ((lambda (name char)
+ (let* ((mark (cdr (assoc (match-string 1 name) qrhl-input--mark-map))))
+ (cl-assert mark)
+ (list (format "\\%s" mark))))
+ (concat "\\`COMBINING \\(" qrhl-input--mark-re "\\)\\(?: ACCENT\\)?\\'"))
+
+ ((lambda (name char)
+ (unless (qrhl-input--ascii-p char)
+ (let* ((mark (cdr (assoc (match-string 1 name) qrhl-input--mark-map))))
+ (cl-assert mark)
+ (list (format "\\%s{}" mark)))))
+ (concat "\\`\\(?:SPACING \\)?\\(" qrhl-input--mark-re "\\)\\(?:
ACCENT\\)?\\'"))
+
+ ("\\AA" ?Å) ;; ("{\\AA}" ?Å)
+ ("\\AE" ?Æ) ;; ("{\\AE}" ?Æ)
+
+ ("$\\times$" ?×) ("\\times" ?×)
+ ("\\O" ?Ø) ;; ("{\\O}" ?Ø)
+ ("\\ss" ?ß) ;; ("{\\ss}" ?ß)
+
+ ("\\aa" ?å) ;; ("{\\aa}" ?å)
+ ("\\ae" ?æ) ;; ("{\\ae}" ?æ)
+
+ ("$\\div$" ?÷) ("\\div" ?÷)
+ ("\\o" ?ø) ;; ("{\\o}" ?ø)
+
+ ("\\~{\\i}" ?ĩ)
+ ("\\={\\i}" ?ī)
+ ("\\u{\\i}" ?ĭ)
+
+ ("\\i" ?ı) ;; ("{\\i}" ?ı)
+ ("\\^{\\j}" ?ĵ)
+
+ ("\\L" ?Ł) ;; ("{\\L}" ?Ł)
+ ("\\l" ?ł) ;; ("{\\l}" ?ł)
+
+ ("\\H" ?̋)
+ ("\\H{}" ?˝)
+ ("\\U{o}" ?ő) ("\\Uo" ?ő) ;; FIXME: Was it just a typo?
+
+ ("\\OE" ?Œ) ;; ("{\\OE}" ?Œ)
+ ("\\oe" ?œ) ;; ("{\\oe}" ?œ)
+
+ ("\\v{\\i}" ?ǐ)
+
+ ("\\={\\AE}" ?Ǣ) ("\\=\\AE" ?Ǣ)
+ ("\\={\\ae}" ?ǣ) ("\\=\\ae" ?ǣ)
+
+ ("\\v{\\j}" ?ǰ)
+ ("\\'{\\AE}" ?Ǽ) ("\\'\\AE" ?Ǽ)
+ ("\\'{\\ae}" ?ǽ) ("\\'\\ae" ?ǽ)
+ ("\\'{\\O}" ?Ǿ) ("\\'\\O" ?Ǿ)
+ ("\\'{\\o}" ?ǿ) ("\\'\\o" ?ǿ)
+
+ ("\\," ? )
+ ("\\/" ?)
+ ("\\:" ? )
+ ("\\;" ? )
+
+
+ ;; ;; Dominique Unruh: Disabling _1 etc.
+ ;; ((lambda (name char)
+ ;; (let* ((base (concat (match-string 1 name) (match-string 3 name)))
+ ;; (basechar (cdr (assoc base (ucs-names)))))
+ ;; (when (qrhl-input--ascii-p basechar)
+ ;; (string (if (match-end 2) ?^ ?_) basechar))))
+ ;; "\\(.*\\)SU\\(?:B\\|\\(PER\\)\\)SCRIPT \\(.*\\)")
+
+ ((lambda (name _char)
+ (let* ((basename (match-string 2 name))
+ (name (if (match-end 1) (capitalize basename) (downcase basename))))
+ (concat "^" (if (> (length name) 1) "\\") name)))
+ "\\`MODIFIER LETTER \\(?:SMALL\\|CAPITA\\(L\\)\\) \\([[:ascii:]]+\\)\\'")
+
+ ;; ((lambda (name char) (format "^%s" (downcase (match-string 1 name))))
+ ;; "\\`MODIFIER LETTER SMALL \\(.\\)\\'")
+ ;; ("^\\1" "\\`MODIFIER LETTER CAPITAL \\(.\\)\\'")
+ ("^o_" ?º)
+ ("^{SM}" ?℠)
+ ("^{TEL}" ?℡)
+ ("^{TM}" ?™)
+
+ ("\\b" ?̱)
+
+ ("\\rq" ?’)
+
+ ;; FIXME: Provides some useful entries (yen, euro, copyright, registered,
+ ;; currency, minus, micro), but also a lot of dubious ones.
+ ((lambda (name char)
+ (unless (or (qrhl-input--ascii-p char)
+ ;; We prefer COMBINING LONG SOLIDUS OVERLAY for \not.
+ (member name '("NOT SIGN")))
+ (concat "\\" (downcase (match-string 1 name)))))
+ "\\`\\([^- ]+\\) SIGN\\'")
+
+ ((lambda (name char)
+ ;; "GREEK SMALL LETTER PHI" (which is \phi) and "GREEK PHI SYMBOL"
+ ;; (which is \varphi) are reversed in `ucs-names', so we define
+ ;; them manually.
+ (unless (string-match-p "\\<PHI\\>" name)
+ (concat "\\" (funcall (if (match-end 1) #' capitalize #'downcase)
+ (match-string 2 name)))))
+ "\\`GREEK \\(?:SMALL\\|CAPITA\\(L\\)\\) LETTER \\([^- ]+\\)\\'")
+
+ ("\\phi" ?ϕ)
+ ("\\Box" ?□)
+ ("\\Bumpeq" ?≎)
+ ("\\Cap" ?⋒)
+ ("\\Cup" ?⋓)
+ ("\\Diamond" ?◇)
+ ("\\Downarrow" ?⇓)
+ ("\\H{o}" ?ő)
+ ("\\Im" ?ℑ)
+ ("\\Join" ?⋈)
+ ("\\Leftarrow" ?⇐)
+ ("\\Leftrightarrow" ?⇔)
+ ("\\Ll" ?⋘)
+ ("\\Lleftarrow" ?⇚)
+ ("\\Longleftarrow" ?⇐)
+ ("\\Longleftrightarrow" ?⇔)
+ ("\\Longrightarrow" ?⇒)
+ ("\\Lsh" ?↰)
+ ("\\Re" ?ℜ)
+ ("\\Rightarrow" ?⇒)
+ ("\\Rrightarrow" ?⇛)
+ ("\\Rsh" ?↱)
+ ("\\Subset" ?⋐)
+ ("\\Supset" ?⋑)
+ ("\\Uparrow" ?⇑)
+ ("\\Updownarrow" ?⇕)
+ ("\\Vdash" ?⊩)
+ ("\\Vert" ?‖)
+ ("\\Vvdash" ?⊪)
+ ("\\aleph" ?ℵ)
+ ("\\amalg" ?∐)
+ ("\\angle" ?∠)
+ ("\\approx" ?≈)
+ ("\\approxeq" ?≊)
+ ("\\ast" ?∗)
+ ("\\asymp" ?≍)
+ ("\\backcong" ?≌)
+ ("\\backepsilon" ?∍)
+ ("\\backprime" ?‵)
+ ("\\backsim" ?∽)
+ ("\\backsimeq" ?⋍)
+ ("\\backslash" ?\\)
+ ("\\barwedge" ?⊼)
+ ("\\because" ?∵)
+ ("\\beth" ?ℶ)
+ ("\\between" ?≬)
+ ("\\bigcap" ?⋂)
+ ("\\bigcirc" ?◯)
+ ("\\bigcup" ?⋃)
+ ("\\bigstar" ?★)
+ ("\\bigtriangledown" ?▽)
+ ("\\bigtriangleup" ?△)
+ ("\\bigvee" ?⋁)
+ ("\\bigwedge" ?⋀)
+ ("\\blacklozenge" ?✦)
+ ("\\blacksquare" ?▪)
+ ("\\blacktriangle" ?▴)
+ ("\\blacktriangledown" ?▾)
+ ("\\blacktriangleleft" ?◂)
+ ("\\blacktriangleright" ?▸)
+ ("\\bot" ?⊥)
+ ("\\bowtie" ?⋈)
+ ("\\boxminus" ?⊟)
+ ("\\boxplus" ?⊞)
+ ("\\boxtimes" ?⊠)
+ ("\\bullet" ?•)
+ ("\\bumpeq" ?≏)
+ ("\\cap" ?∩)
+ ("\\cdots" ?⋯)
+ ("\\centerdot" ?⋅)
+ ("\\checkmark" ?✓)
+ ("\\chi" ?χ)
+ ("\\circ" ?∘)
+ ("\\circeq" ?≗)
+ ("\\circlearrowleft" ?↺)
+ ("\\circlearrowright" ?↻)
+ ("\\circledR" ?®)
+ ("\\circledS" ?Ⓢ)
+ ("\\circledast" ?⊛)
+ ("\\circledcirc" ?⊚)
+ ("\\circleddash" ?⊝)
+ ("\\clubsuit" ?♣)
+ ("\\coloneq" ?≔)
+ ("\\complement" ?∁)
+ ("\\cong" ?≅)
+ ("\\coprod" ?∐)
+ ("\\cup" ?∪)
+ ("\\curlyeqprec" ?⋞)
+ ("\\curlyeqsucc" ?⋟)
+ ("\\curlypreceq" ?≼)
+ ("\\curlyvee" ?⋎)
+ ("\\curlywedge" ?⋏)
+ ("\\curvearrowleft" ?↶)
+ ("\\curvearrowright" ?↷)
+
+ ("\\dag" ?†)
+ ("\\dagger" ?†)
+ ("\\daleth" ?ℸ)
+ ("\\dashv" ?⊣)
+ ("\\ddag" ?‡)
+ ("\\ddagger" ?‡)
+ ("\\ddots" ?⋱)
+ ("\\diamond" ?⋄)
+ ("\\diamondsuit" ?♢)
+ ("\\divideontimes" ?⋇)
+ ("\\doteq" ?≐)
+ ("\\doteqdot" ?≑)
+ ("\\dotplus" ?∔)
+ ("\\dotsquare" ?⊡)
+ ("\\downarrow" ?↓)
+ ("\\downdownarrows" ?⇊)
+ ("\\downleftharpoon" ?⇃)
+ ("\\downrightharpoon" ?⇂)
+ ("\\ell" ?ℓ)
+ ("\\emptyset" ?∅)
+ ("\\eqcirc" ?≖)
+ ("\\eqcolon" ?≕)
+ ("\\eqslantgtr" ?⋝)
+ ("\\eqslantless" ?⋜)
+ ("\\equiv" ?≡)
+ ("\\exists" ?∃)
+ ("\\fallingdotseq" ?≒)
+ ("\\flat" ?♭)
+ ("\\forall" ?∀)
+ ("\\frac1" ?⅟)
+ ("\\frac12" ?½)
+ ("\\frac13" ?⅓)
+ ("\\frac14" ?¼)
+ ("\\frac15" ?⅕)
+ ("\\frac16" ?⅙)
+ ("\\frac18" ?⅛)
+ ("\\frac23" ?⅔)
+ ("\\frac25" ?⅖)
+ ("\\frac34" ?¾)
+ ("\\frac35" ?⅗)
+ ("\\frac38" ?⅜)
+ ("\\frac45" ?⅘)
+ ("\\frac56" ?⅚)
+ ("\\frac58" ?⅝)
+ ("\\frac78" ?⅞)
+ ("\\frown" ?⌢)
+ ("\\ge" ?≥)
+ ("\\geq" ?≥)
+ ("\\geqq" ?≧)
+ ("\\geqslant" ?≥)
+ ("\\gets" ?←)
+ ("\\gg" ?≫)
+ ("\\ggg" ?⋙)
+ ("\\gimel" ?ℷ)
+ ("\\gnapprox" ?⋧)
+ ("\\gneq" ?≩)
+ ("\\gneqq" ?≩)
+ ("\\gnsim" ?⋧)
+ ("\\gtrapprox" ?≳)
+ ("\\gtrdot" ?⋗)
+ ("\\gtreqless" ?⋛)
+ ("\\gtreqqless" ?⋛)
+ ("\\gtrless" ?≷)
+ ("\\gtrsim" ?≳)
+ ("\\gvertneqq" ?≩)
+ ("\\hbar" ?ℏ)
+ ("\\heartsuit" ?♥)
+ ("\\hookleftarrow" ?↩)
+ ("\\hookrightarrow" ?↪)
+ ("\\iff" ?⇔)
+ ("\\imath" ?ı)
+ ("\\in" ?∈)
+ ("\\infty" ?∞)
+ ("\\int" ?∫)
+ ("\\intercal" ?⊺)
+ ("\\langle" ?⟨) ;; Was ?〈, see bug#12948.
+ ("\\lbrace" ?{)
+ ("\\lbrack" ?\[)
+ ("\\lceil" ?⌈)
+ ("\\ldots" ?…)
+ ("\\le" ?≤)
+ ("\\leadsto" ?↝)
+ ("\\leftarrow" ?←)
+ ("\\leftarrowtail" ?↢)
+ ("\\leftharpoondown" ?↽)
+ ("\\leftharpoonup" ?↼)
+ ("\\leftleftarrows" ?⇇)
+ ;; ("\\leftparengtr" ?〈), see bug#12948.
+ ("\\leftrightarrow" ?↔)
+ ("\\leftrightarrows" ?⇆)
+ ("\\leftrightharpoons" ?⇋)
+ ("\\leftrightsquigarrow" ?↭)
+ ("\\leftthreetimes" ?⋋)
+ ("\\leq" ?≤)
+ ("\\leqq" ?≦)
+ ("\\leqslant" ?≤)
+ ("\\lessapprox" ?≲)
+ ("\\lessdot" ?⋖)
+ ("\\lesseqgtr" ?⋚)
+ ("\\lesseqqgtr" ?⋚)
+ ("\\lessgtr" ?≶)
+ ("\\lesssim" ?≲)
+ ("\\lfloor" ?⌊)
+ ("\\lhd" ?◁)
+ ("\\rhd" ?▷)
+ ("\\ll" ?≪)
+ ("\\llcorner" ?⌞)
+ ("\\lnapprox" ?⋦)
+ ("\\lneq" ?≨)
+ ("\\lneqq" ?≨)
+ ("\\lnsim" ?⋦)
+ ("\\longleftarrow" ?←)
+ ("\\longleftrightarrow" ?↔)
+ ("\\longmapsto" ?↦)
+ ("\\longrightarrow" ?→)
+ ("\\looparrowleft" ?↫)
+ ("\\looparrowright" ?↬)
+ ("\\lozenge" ?✧)
+ ("\\lq" ?‘)
+ ("\\lrcorner" ?⌟)
+ ("\\ltimes" ?⋉)
+ ("\\lvertneqq" ?≨)
+ ("\\maltese" ?✠)
+ ("\\mapsto" ?↦)
+ ("\\measuredangle" ?∡)
+ ("\\mho" ?℧)
+ ("\\mid" ?∣)
+ ("\\models" ?⊧)
+ ("\\mp" ?∓)
+ ("\\multimap" ?⊸)
+ ("\\nLeftarrow" ?⇍)
+ ("\\nLeftrightarrow" ?⇎)
+ ("\\nRightarrow" ?⇏)
+ ("\\nVDash" ?⊯)
+ ("\\nVdash" ?⊮)
+ ("\\nabla" ?∇)
+ ("\\napprox" ?≉)
+ ("\\natural" ?♮)
+ ("\\ncong" ?≇)
+ ("\\ne" ?≠)
+ ("\\nearrow" ?↗)
+ ("\\neg" ?¬)
+ ("\\neq" ?≠)
+ ("\\nequiv" ?≢)
+ ("\\newline" ?
)
+ ("\\nexists" ?∄)
+ ("\\ngeq" ?≱)
+ ("\\ngeqq" ?≱)
+ ("\\ngeqslant" ?≱)
+ ("\\ngtr" ?≯)
+ ("\\ni" ?∋)
+ ("\\nleftarrow" ?↚)
+ ("\\nleftrightarrow" ?↮)
+ ("\\nleq" ?≰)
+ ("\\nleqq" ?≰)
+ ("\\nleqslant" ?≰)
+ ("\\nless" ?≮)
+ ("\\nmid" ?∤)
+ ("\\not" ?̸) ;FIXME: conflict with "NOT SIGN" ¬.
+ ("\\notin" ?∉)
+ ("\\nparallel" ?∦)
+ ("\\nprec" ?⊀)
+ ("\\npreceq" ?⋠)
+ ("\\nrightarrow" ?↛)
+ ("\\nshortmid" ?∤)
+ ("\\nshortparallel" ?∦)
+ ("\\nsim" ?≁)
+ ("\\nsimeq" ?≄)
+ ("\\nsubset" ?⊄)
+ ("\\nsubseteq" ?⊈)
+ ("\\nsubseteqq" ?⊈)
+ ("\\nsucc" ?⊁)
+ ("\\nsucceq" ?⋡)
+ ("\\nsupset" ?⊅)
+ ("\\nsupseteq" ?⊉)
+ ("\\nsupseteqq" ?⊉)
+ ("\\ntriangleleft" ?⋪)
+ ("\\ntrianglelefteq" ?⋬)
+ ("\\ntriangleright" ?⋫)
+ ("\\ntrianglerighteq" ?⋭)
+ ("\\nvDash" ?⊭)
+ ("\\nvdash" ?⊬)
+ ("\\nwarrow" ?↖)
+ ("\\odot" ?⊙)
+ ("\\oint" ?∮)
+ ("\\ominus" ?⊖)
+ ("\\oplus" ?⊕)
+ ("\\oslash" ?⊘)
+ ("\\otimes" ?⊗)
+ ("\\par" ?
)
+ ("\\parallel" ?∥)
+ ("\\partial" ?∂)
+ ("\\perp" ?⊥)
+ ("\\pitchfork" ?⋔)
+ ("\\prec" ?≺)
+ ("\\precapprox" ?≾)
+ ("\\preceq" ?≼)
+ ("\\precnapprox" ?⋨)
+ ("\\precnsim" ?⋨)
+ ("\\precsim" ?≾)
+ ("\\prime" ?′)
+ ("\\prod" ?∏)
+ ("\\propto" ?∝)
+ ("\\qed" ?∎)
+ ("\\quad" ? )
+ ("\\rangle" ?\⟩) ;; Was ?〉, see bug#12948.
+ ("\\rbrace" ?})
+ ("\\rbrack" ?\])
+ ("\\rceil" ?⌉)
+ ("\\rfloor" ?⌋)
+ ("\\rightarrow" ?→)
+ ("\\rightarrowtail" ?↣)
+ ("\\rightharpoondown" ?⇁)
+ ("\\rightharpoonup" ?⇀)
+ ("\\rightleftarrows" ?⇄)
+ ("\\rightleftharpoons" ?⇌)
+ ;; ("\\rightparengtr" ?⦔) ;; Was ?〉, see bug#12948.
+ ("\\rightrightarrows" ?⇉)
+ ("\\rightthreetimes" ?⋌)
+ ("\\risingdotseq" ?≓)
+ ("\\rtimes" ?⋊)
+ ("\\sbs" ?﹨)
+ ("\\searrow" ?↘)
+ ("\\setminus" ?∖)
+ ("\\sharp" ?♯)
+ ("\\shortmid" ?∣)
+ ("\\shortparallel" ?∥)
+ ("\\sim" ?∼)
+ ("\\simeq" ?≃)
+ ("\\smallamalg" ?∐)
+ ("\\smallsetminus" ?∖)
+ ("\\smallsmile" ?⌣)
+ ("\\smile" ?⌣)
+ ("\\spadesuit" ?♠)
+ ("\\sphericalangle" ?∢)
+ ("\\sqcap" ?⊓)
+ ("\\sqcup" ?⊔)
+ ("\\sqsubset" ?⊏)
+ ("\\sqsubseteq" ?⊑)
+ ("\\sqsupset" ?⊐)
+ ("\\sqsupseteq" ?⊒)
+ ("\\square" ?□)
+ ("\\squigarrowright" ?⇝)
+ ("\\star" ?⋆)
+ ("\\straightphi" ?φ)
+ ("\\subset" ?⊂)
+ ("\\subseteq" ?⊆)
+ ("\\subseteqq" ?⊆)
+ ("\\subsetneq" ?⊊)
+ ("\\subsetneqq" ?⊊)
+ ("\\succ" ?≻)
+ ("\\succapprox" ?≿)
+ ("\\succcurlyeq" ?≽)
+ ("\\succeq" ?≽)
+ ("\\succnapprox" ?⋩)
+ ("\\succnsim" ?⋩)
+ ("\\succsim" ?≿)
+ ("\\sum" ?∑)
+ ("\\supset" ?⊃)
+ ("\\supseteq" ?⊇)
+ ("\\supseteqq" ?⊇)
+ ("\\supsetneq" ?⊋)
+ ("\\supsetneqq" ?⊋)
+ ("\\surd" ?√)
+ ("\\swarrow" ?↙)
+ ("\\therefore" ?∴)
+ ("\\thickapprox" ?≈)
+ ("\\thicksim" ?∼)
+ ("\\to" ?→)
+ ("\\top" ?⊤)
+ ("\\triangle" ?▵)
+ ("\\triangledown" ?▿)
+ ("\\triangleleft" ?◃)
+ ("\\trianglelefteq" ?⊴)
+ ("\\triangleq" ?≜)
+ ("\\triangleright" ?▹)
+ ("\\trianglerighteq" ?⊵)
+ ("\\twoheadleftarrow" ?↞)
+ ("\\twoheadrightarrow" ?↠)
+ ("\\ulcorner" ?⌜)
+ ("\\uparrow" ?↑)
+ ("\\updownarrow" ?↕)
+ ("\\upleftharpoon" ?↿)
+ ("\\uplus" ?⊎)
+ ("\\uprightharpoon" ?↾)
+ ("\\upuparrows" ?⇈)
+ ("\\urcorner" ?⌝)
+ ("\\u{i}" ?ĭ)
+ ("\\vDash" ?⊨)
+
+ ((lambda (name char)
+ ;; "GREEK SMALL LETTER PHI" (which is \phi) and "GREEK PHI SYMBOL"
+ ;; (which is \varphi) are reversed in `ucs-names', so we define
+ ;; them manually.
+ (unless (string-match-p "\\<PHI\\>" name)
+ (concat "\\var" (downcase (match-string 1 name)))))
+ "\\`GREEK \\([^- ]+\\) SYMBOL\\'")
+
+ ("\\varphi" ?φ)
+ ("\\varprime" ?′)
+ ("\\varpropto" ?∝)
+ ("\\varsigma" ?ς)
+ ("\\vartriangleleft" ?⊲)
+ ("\\vartriangleright" ?⊳)
+ ("\\vdash" ?⊢)
+ ("\\vdots" ?⋮)
+ ("\\vee" ?∨)
+ ("\\veebar" ?⊻)
+ ("\\vert" ?|)
+ ("\\wedge" ?∧)
+ ("\\wp" ?℘)
+ ("\\wr" ?≀)
+
+ ("\\Bbb{N}" ?ℕ) ; AMS commands for blackboard bold
+ ("\\Bbb{P}" ?ℙ) ; Also sometimes \mathbb.
+ ("\\Bbb{R}" ?ℝ)
+ ("\\Bbb{Z}" ?ℤ)
+ ("--" ?–)
+ ("---" ?—)
+ ;; We used to use ~ for NBSP but that's inconvenient and may even look like
+ ;; a bug where the user finds his ~ key doesn't insert a ~ any more.
+ ("\\ " ? )
+ ("\\\\" ?\\)
+ ("\\mathscr{I}" ?ℐ) ; moment of inertia
+ ("\\Smiley" ?☺)
+ ("\\blacksmiley" ?☻)
+ ("\\Frowny" ?☹)
+ ("\\Letter" ?✉)
+ ("\\permil" ?‰)
+ ;; Probably not useful enough:
+ ;; ("\\Telefon" ?☎) ; there are other possibilities
+ ;; ("\\Radioactivity" ?☢)
+ ;; ("\\Biohazard" ?☣)
+ ;; ("\\Male" ?♂)
+ ;; ("\\Female" ?♀)
+ ;; ("\\Lightning" ?☇)
+ ;; ("\\Mercury" ?☿)
+ ;; ("\\Earth" ?♁)
+ ;; ("\\Jupiter" ?♃)
+ ;; ("\\Saturn" ?♄)
+ ;; ("\\Uranus" ?♅)
+ ;; ("\\Neptune" ?♆)
+ ;; ("\\Pluto" ?♇)
+ ;; ("\\Sun" ?☉)
+ ;; ("\\Writinghand" ?✍)
+ ;; ("\\Yinyang" ?☯)
+ ;; ("\\Heart" ?♡)
+ ("\\dh" ?ð)
+ ("\\DH" ?Ð)
+ ("\\th" ?þ)
+ ("\\TH" ?Þ)
+ ("\\lnot" ?¬)
+ ("\\ordfeminine" ?ª)
+ ("\\ordmasculine" ?º)
+ ("\\lambdabar" ?ƛ)
+ ("\\celsius" ?℃)
+ ;; by analogy with lq, rq:
+ ("\\ldq" ?\“)
+ ("\\rdq" ?\”)
+ ("\\defs" ?≙) ; per fuzz/zed
+ ;; ("\\sqrt[3]" ?∛)
+ ("\\llbracket" ?\⟦) ; stmaryrd
+ ("\\rrbracket" ?\⟧)
+ ;; ("\\lbag" ?\〚) ; fuzz
+ ;; ("\\rbag" ?\〛)
+ ("\\ldata" ?\《) ; fuzz/zed
+ ("\\rdata" ?\》)
+ ;; From Karl Eichwalder.
+ ("\\glq" ?‚)
+ ("\\grq" ?‘)
+ ("\\glqq" ?„) ("\\\"`" ?„)
+ ("\\grqq" ?“) ("\\\"'" ?“)
+ ("\\flq" ?‹)
+ ("\\frq" ?›)
+ ("\\flqq" ?\«) ("\\\"<" ?\«)
+ ("\\frqq" ?\») ("\\\">" ?\»)
+
+ ("\\-" ?) ;; soft hyphen
+
+ ("\\textmu" ?µ)
+ ("\\textfractionsolidus" ?⁄)
+ ("\\textbigcircle" ?⃝)
+ ("\\textmusicalnote" ?♪)
+ ("\\textdied" ?✝)
+ ("\\textcolonmonetary" ?₡)
+ ("\\textwon" ?₩)
+ ("\\textnaira" ?₦)
+ ("\\textpeso" ?₱)
+ ("\\textlira" ?₤)
+ ("\\textrecipe" ?℞)
+ ("\\textinterrobang" ?‽)
+ ("\\textpertenthousand" ?‱)
+ ("\\textbaht" ?฿)
+ ("\\textnumero" ?№)
+ ("\\textdiscount" ?⁒)
+ ("\\textestimated" ?℮)
+ ("\\textopenbullet" ?◦)
+ ("\\textlquill" ?\⁅)
+ ("\\textrquill" ?\⁆)
+ ("\\textcircledP" ?℗)
+ ("\\textreferencemark" ?※)
+ )
+
+
+;; Dominique's rules for qrhl-tool:
+(quail-define-rules
+ ((append . t))
+ ("\\ox" ?⊗)
+ ("\\ket" ["|⟩"])
+ ("\\ket0" ["|0⟩"])
+ ("\\ket1" ["|1⟩"])
+ ("[|" ["⟦"])
+ ("|]" ["⟧"])
+ (">>" ?»)
+ ("\\Cla" ["ℭ𝔩𝔞"])
+ ("\\qeq" ["≡𝔮"])
+ )
+
+(provide 'qrhl-input)
+
+;;; qrhl-input.el ends here
diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el
new file mode 100644
index 0000000000..bd0ec6290b
--- /dev/null
+++ b/qrhl/qrhl.el
@@ -0,0 +1,140 @@
+;;; qrhl.el --- Mode for qrhl-tool theorem prover -*- lexical-binding: t -*-
+
+;; This file is part of Proof General.
+
+;; Copyright © 2017–2022 University of Tartu
+
+;; Author: Dominique Unruh
+
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+
+;; See also https://dominique-unruh.github.io/qrhl-tool/
+
+;;; Code:
+
+(if (version< emacs-version "26")
+ (require 'qrhl-input-25)
+ (require 'qrhl-input))
+
+
+(defcustom qrhl-input-method "qrhl" "Input method to use when editing qRHL
proof scripts"
+ :type '(string) :group 'qrhl)
+
+(defcustom qrhl-prog-name "qrhl" "Name/path of the qrhl-prover command.
(Restart Emacs after changing this.)"
+ :type '(string) :group 'qrhl)
+
+(defun qrhl-find-and-forget (span)
+ (proof-generic-count-undos span))
+
+(defvar qrhl-focus-cmd-regexp
+ (let* ((number "[0-9]+")
+ (white "[[:blank:]]*")
+ (number-or-range (concat number "\\(" white "-" white number
"\\)?"))
+ (range-list (concat number-or-range "\\(" white "," white
number-or-range "\\)*"))
+ (focus-label "\\({\\|}\\|[+*-]+\\)")
+ (focus-cmd (concat "\\(" range-list white ":" white "\\)?"
focus-label))
+ )
+ focus-cmd))
+
+(defun qrhl-forward-regex (regex)
+ "If text starting at point matches REGEX, move to end of the match and
return t.
+ Otherwise return nil"
+ (and (looking-at regex) (goto-char (match-end 0)) t))
+
+(defun qrhl-parse-regular-command ()
+ "Finds the period-terminated command starting at the point (and moves to its
end).
+ Returns t if this worked."
+ (let ((pos
+ (save-excursion
+ (progn
+ (while (or
+ ; skip forward over regular chars, period with non-white,
quoted string
+ (qrhl-forward-regex "\\([^.{(\"]+\\|\\.[^
\t\n]\\|\"\\([^\"]+\\)\"\\)")
+ (and (looking-at "[{(]") (forward-list))
+ ))
+ (and (qrhl-forward-regex "\\.") (point))
+ ))))
+ (princ pos)
+ (and pos (goto-char pos) t)))
+
+(defun qrhl-parse-focus-command ()
+ (and (looking-at qrhl-focus-cmd-regexp)
+ (goto-char (match-end 0))))
+
+(defun qrhl-proof-script-parse-function ()
+ "Finds the command/comment starting at the point"
+ (or (and (qrhl-forward-regex "#[^\n]*\n") 'comment)
+ (and (qrhl-parse-focus-command) 'cmd)
+ (and (qrhl-parse-regular-command) 'cmd)))
+
+(defvar qrhl-font-lock-subsuperscript
+ '(("\\(⇩\\)\\([^[:space:]]\\)" .
+ ((2 '(face subscript display (raise -0.3)))
+ (1 '(face nil display ""))))
+ ("\\(⇧\\)\\([^[:space:]]\\)" .
+ ((2 '(face superscript display (raise 0.3)))
+ (1 '(face nil display "")))))
+ "Font-lock configuration for displaying sub/superscripts that are prefixed
by ⇩/⇧")
+
+(defvar qrhl-font-lock-keywords
+ ; Very simple configuration of keywords: highlights all occurrences, even if
they are not actually keywords (e.g., when they are part of a term)
+ (append qrhl-font-lock-subsuperscript
+ '("lemma" "qrhl" "include" "quantum" "program" "equal" "simp"
"isabelle" "isa" "var" "qed"
+ "skip"))
+ "Font-lock configuration for qRHL proof scripts")
+
+(proof-easy-config 'qrhl "qRHL"
+ proof-prog-name qrhl-prog-name
+ ; We need to give some option here, otherwise
proof-prog-name is interpreted
+ ; as a shell command which leads to problems if the path
contains spaces
+ ; (see the documentation for proof-prog-name)
+ qrhl-prog-args '("--emacs")
+ ;proof-script-command-end-regexp "\\.[ \t]*$"
+ proof-script-parse-function 'qrhl-proof-script-parse-function
+ proof-shell-annotated-prompt-regexp
"^\\(\\.\\.\\.\\|qrhl\\)> "
+ ;proof-script-comment-start-regexp "#"
+ ;proof-script-comment-end "\n"
+ proof-shell-error-regexp "^\\(\\[ERROR\\]\\|Exception\\)"
+ proof-undo-n-times-cmd "undo %s."
+ proof-find-and-forget-fn 'qrhl-find-and-forget
+ proof-shell-start-goals-regexp "^[0-9]+
subgoals:\\|^Goal:\\|^No current goal\\.\\|^In cheat mode\\.\\|^No focused
goals (use "
+ proof-shell-proof-completed-regexp "^No current goal.$"
+ proof-shell-eager-annotation-start "\\*\\*\\* "
+ proof-shell-eager-annotation-start-length 4
+ proof-no-fully-processed-buffer t
+ proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" .
"\\\""))
+ proof-shell-cd-cmd "changeDirectory \"%s\"."
+ proof-save-command-regexp "^adfuaisdfaoidsfasd" ;
ProofGeneral produces warning when this is not set. But we don't want goal/save
commands to be recognized because that makes ProofGeneral do an atomic undo.
+ proof-tree-external-display nil
+ proof-script-font-lock-keywords qrhl-font-lock-keywords
+ proof-goals-font-lock-keywords qrhl-font-lock-keywords
+ proof-response-font-lock-keywords qrhl-font-lock-keywords
+ proof-shell-unicode t
+ )
+
+; buttoning functions follow https://superuser.com/a/331896/748969
+(define-button-type 'qrhl-find-file-button
+ 'follow-link t
+ 'action #'qrhl-find-file-button)
+
+(defun qrhl-find-file-button (button)
+ (find-file (buffer-substring (button-start button) (button-end button))))
+
+(defun qrhl-buttonize-buffer ()
+ "Turn all include commands in a qRHL proof script into clickable buttons"
+ (interactive)
+ (remove-overlays)
+ (save-excursion
+ (goto-char (point-min))
+ (while (re-search-forward "include\s*\"\\([^\"]+\\)\"\s*\\." nil t)
+ (make-button (match-beginning 1) (match-end 1) :type
'qrhl-find-file-button))))
+
+(add-hook 'qrhl-mode-hook
+ (lambda ()
+ (set-input-method qrhl-input-method)
+ (set-variable 'electric-indent-mode nil t)
+ (qrhl-buttonize-buffer)))
+
+(provide 'qrhl)
- [nongnu] elpa/proof-general 543aa777d7 14/25: Made path to qrhl-tool customizable., (continued)
- [nongnu] elpa/proof-general 543aa777d7 14/25: Made path to qrhl-tool customizable., ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 232c7ccae1 18/25: qrhl: Ensure UTF-8 via `proof-shell-unicode` instead of `set-language-environment`., ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general ff22652025 17/25: qrhl: Font-lock support (keywords and sub/superscripts), ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general b49220f634 01/25: Added qRHL support from qrhl-tool repo, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 80aac72a7a 02/25: Fix: proof-tree-external-display := nil, otherwise ProofGeneral fails, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general ee01e75c66 03/25: qrhl-mode recognizes focus commands (e.g. '1-2: ++'), ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 9b3ec8c596 16/25: qrhl: Made variable setting of `electric-indent-mode` buffer-local, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 67006d14e3 15/25: Merge branch 'master' into qrhl-tool, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 30b882b8c3 04/25: qrhl.el: Fixed regexp for errors, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general df4013732e 22/25: qrhl: Removed autoload cookie from customizable options., ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general fe8b9fccb3 25/25: Merge pull request #636 from dominique-unruh/qrhl-tool,
ELPA Syncer <=
- [nongnu] elpa/proof-general 847492f78f 13/25: Using require instead of load-library to load qrhl-input., ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 0eb165d2a5 12/25: Removed some hardcoded configuration in qrhl mode:, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 360b6c24e3 24/25: Clarified copyright of qrhl: University of Tartu, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general e86aa8468b 07/25: Added author to qrhl.el., ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 0e51f5af9a 06/25: Merge remote-tracking branch 'origin/master' into qrhl-tool, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general afb17bbee9 21/25: qrhl: Updated copyright headers. Set lexical-binding: t, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general dead1cc989 23/25: Updated doc-magic (`make -C doc magic`), ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general aa086d8b83 19/25: Annotated qrhl-input.el with the changes w.r.t. Emacs's latin-ltx.el, ELPA Syncer, 2022/02/28
- [nongnu] elpa/proof-general 1787acf784 20/25: Support for Emacs 25 in qrhl: Creating separate input method file qrhl-input-25.el that supports Emacs 25., ELPA Syncer, 2022/02/28