[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]

branch: elpa/proof-general
commit 1787acf784151434e6266c609a122d7a62eab5eb
Author: Dominique Unruh <unruh@ut.ee>
Commit: Dominique Unruh <unruh@ut.ee>

    Support for Emacs 25 in qrhl: Creating separate input method file 
qrhl-input-25.el that supports Emacs 25.
    
    ..
---
 qrhl/qrhl-input-25.el | 747 ++++++++++++++++++++++++++++++++++++++++++++++++++
 qrhl/qrhl.el          |   5 +-
 2 files changed, 751 insertions(+), 1 deletion(-)

diff --git a/qrhl/qrhl-input-25.el b/qrhl/qrhl-input-25.el
new file mode 100644
index 0000000000..803292327c
--- /dev/null
+++ b/qrhl/qrhl-input-25.el
@@ -0,0 +1,747 @@
+;;; qrhl-input.el --- Quail package for TeX-style input -*-coding: utf-8;-*-
+
+;; 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
+
+;; Author: TAKAHASHI Naoto <ntakahas@m17n.org>
+;;         Dave Love <fx@gnu.org>
+;; Keywords: multilingual, input, Greek, i18n
+
+;; Author: Dominique Unruh <unruh@ut.ee>
+
+;; 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
+
+;; This version is for Emacs 25 since 'qrhl-input.el' is incompatible with 
Emacs 25.
+
+(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.el b/qrhl/qrhl.el
index bf3a14e74f..7bda3eb8f6 100644
--- a/qrhl/qrhl.el
+++ b/qrhl/qrhl.el
@@ -1,6 +1,9 @@
 ;; Author: Dominique Unruh
 
-(require 'qrhl-input)
+(if (version< emacs-version "26")
+    (require 'qrhl-input-25)
+  (require 'qrhl-input))
+
 
 ;;;###autoload
 (defgroup qrhl nil "qRHL prover settings")