[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general a5021b929f 7/7: Merge pull request #643 from
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general a5021b929f 7/7: Merge pull request #643 from dominique-unruh/qrhl-tool |
|
Date: |
Thu, 10 Mar 2022 10:58:33 -0500 (EST) |
branch: elpa/proof-general
commit a5021b929f21e2a478ca803be68e7b48c4752851
Merge: d9cfe74845 07e6b0d4e5
Author: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Commit: GitHub <noreply@github.com>
Merge pull request #643 from dominique-unruh/qrhl-tool
Fix byte-compilation problems
---
.github/workflows/test.yml | 4 +
Makefile | 2 +-
ci/simple-tests/README.md | 2 +
ci/simple-tests/test-qrhl.el | 24 ++
proof-general.el | 2 +-
qrhl/qrhl-input-25.el | 753 -------------------------------------------
qrhl/qrhl-input.el | 30 +-
qrhl/qrhl.el | 77 +++--
8 files changed, 90 insertions(+), 804 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 826ed743af..57296e8d49 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -252,3 +252,7 @@ jobs:
- run: emacs --version
- run: make -C ci/test-indent
+
+ # Testing this here because this job runs with all Emacs versions
+ - run: make -C ci/simple-tests test-qrhl.success
+
diff --git a/Makefile b/Makefile
index e441e3d19b..4d8f51ccab 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
# subdirectories for provers: to be compiled and installed
-PROVERS=coq easycrypt pghaskell pgocaml pgshell phox
+PROVERS=coq easycrypt pghaskell pgocaml pgshell phox qrhl
# generic lisp code: to be compiled and installed
OTHER_ELISP=generic lib
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 34812cf444..03f4183ac8 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -12,6 +12,8 @@ coq-par-job-needs-compilation-quick
possible cases
test-prelude-correct
: test that the Proof General prelude is correct
+test-qrhl
+: tests relating to the qRHL prover
# Important conventions
diff --git a/ci/simple-tests/test-qrhl.el b/ci/simple-tests/test-qrhl.el
new file mode 100644
index 0000000000..0f00e2bd7f
--- /dev/null
+++ b/ci/simple-tests/test-qrhl.el
@@ -0,0 +1,24 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2022 Dominique Unruh
+;;
+;; Authors: Dominique Unruh
+;; Maintainer: Dominique Unruh
+;;
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Tests related to the qRHL prover
+;;
+
+(ert-deftest load-qrhl-input ()
+ :expected-result :passed
+ "Test that the qRHL input method loads without errors in .qrhl files"
+
+ (message "load-qrhl-input test: Check loading of qRHL input method")
+ (find-file "test.qrhl")
+ ;; Ideally we would do some simulated keypresses and check whether they
+ ;; are translated correctly. But I don't know how. (Dominique)
+ (should (string= current-input-method "qrhl"))
+ )
diff --git a/proof-general.el b/proof-general.el
index fc9853f67e..b583bcdf61 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -77,7 +77,7 @@
;; the corresponding file.
(let ((byte-compile-directories
'("generic" "lib"
- "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
+ "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox" "qrhl"
)))
(dolist (dir byte-compile-directories)
(add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
diff --git a/qrhl/qrhl-input-25.el b/qrhl/qrhl-input-25.el
deleted file mode 100644
index 6d9fb574ac..0000000000
--- a/qrhl/qrhl-input-25.el
+++ /dev/null
@@ -1,753 +0,0 @@
-;;; 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
index 8cc520425c..8d7bc41e46 100644
--- a/qrhl/qrhl-input.el
+++ b/qrhl/qrhl-input.el
@@ -1,8 +1,7 @@
-;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in
ProofGeneral -*-coding: utf-8;-*-
+;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in
ProofGeneral -*- lexical-binding: t -*-
-;; Copyright (C) 2001-2018 Free Software Foundation, Inc.
-;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009,
-;; 2010, 2011
+;; Copyright (C) 2001-2022 Free Software Foundation, Inc.
+;; Copyright (C) 2001-2011
;; National Institute of Advanced Industrial Science and Technology (AIST)
;; Registration Number H14PRO021
;; Copyright (C) 2017-2022 University of Tartu
@@ -18,19 +17,16 @@
;; 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
+;; - Made code compatible with Emacs 25 (@monnier)
;;; Code:
-(if (version< emacs-version "26")
- (error "Emacs version >= 26 required"))
-
(require 'quail)
(quail-define-package
@@ -71,22 +67,28 @@
(pcase rule
(`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule.
(`(,seq ,re)
- (let ((count 0)
- (re (eval re t)))
- (maphash
+ (let* ((count 0)
+ (re (eval re t))
+ (ucs-names (ucs-names))
+ (process-one-entry
(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))))
+ (funcall (eval seq t) 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))
+ (push (list keys char) newrules)))))))
+ ;; Emacs-25's `ucs-names' returned an alist rather than a hash
+ ;; table and that changed to a hash-table in Emacs-26.
+ (if (hash-table-p ucs-names)
+ (maphash process-one-entry ucs-names)
+ (dolist (pair ucs-names)
+ (funcall process-one-entry (car pair) (cdr pair))))
;; (message "qrhl-input: %d mappings for %S" count re)
))))
(setq newrules (delete-dups newrules))
diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el
index bd0ec6290b..d5af5661c2 100644
--- a/qrhl/qrhl.el
+++ b/qrhl/qrhl.el
@@ -14,15 +14,18 @@
;;; Code:
-(if (version< emacs-version "26")
- (require 'qrhl-input-25)
- (require 'qrhl-input))
+(require 'proof)
+(require 'proof-easy-config)
+(require 'proof-script) ;For proof-generic-count-undos.
+(require 'qrhl-input)
-(defcustom qrhl-input-method "qrhl" "Input method to use when editing qRHL
proof scripts"
+(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.)"
+(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)
@@ -44,10 +47,11 @@
(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).
+ "Find the period-terminated command starting at point.
+ Moves to its end.
Returns t if this worked."
- (let ((pos
- (save-excursion
+ (let ((pos
+ (save-excursion
(progn
(while (or
; skip forward over regular chars, period with non-white,
quoted string
@@ -86,33 +90,36 @@
"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
- )
+ 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 file name
+ ;; 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\"."
+ ;; 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-save-command-regexp "\\`a\\`" ;AKA `regexp-unmatchable' in Emacs-27
+ 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
- [nongnu] elpa/proof-general updated (d9cfe74845 -> a5021b929f), ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general 1a64e61c93 2/7: Added "qrhl" to the list of byte-compiled directories., ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general 07e6b0d4e5 6/7: Made qrhl-input.el compile on all supported Emacs versions., ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general a0ebe26bbe 5/7: tests: Add test whether qrhl input method loads correctly, ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general 5ecce84864 1/7: qrhl: Added both `(require 'proof)` and `(require 'proof-easy-config)'., ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general 3f5fe71e52 3/7: Miscelleaneous cleanup in qrhl.el (by @monnier), ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general 2856783ddd 4/7: Makefile: Added qrhl to provers that need to be compiled, ELPA Syncer, 2022/03/10
- [nongnu] elpa/proof-general a5021b929f 7/7: Merge pull request #643 from dominique-unruh/qrhl-tool,
ELPA Syncer <=