diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2010-09-01 13:34:37 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-01 13:34:37 +0000 |
commit | c1955a6fa62b94b1906a199638caf293f29319a8 (patch) | |
tree | 37a6c650c07539b1686d02ad7bc3876b0627efca | |
parent | 06fb36588deb414cbe62699dc8ec2292aa9c8a71 (diff) |
Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp
instead of pure strings.
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | coq/coq-indent.el | 21 | ||||
-rw-r--r-- | coq/coq-syntax.el | 46 | ||||
-rw-r--r-- | coq/coq.el | 12 |
4 files changed, 50 insertions, 33 deletions
@@ -70,7 +70,6 @@ *** "Movie" output: export an annotated buffer in XML Basic movie output for Proviola, see http://mws.cs.ru.nl/proviola - ** Isabelle/Isar changes *** Support undo back into completed proofs (linear_undo). @@ -84,13 +83,14 @@ *** Isabelle Settings now organised in sub-menus - ** Coq changes *** Only supports Coq 8.1+, support for earlier versions dropped. *** Holes mode can be turned on/off and has its own minor mode +*** Some keyboard shortcuts are now available in goals buffer + C-c C-a C-<c,p,o,b,a> are now available in goal buffer. ** Notable internal changes diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 64a36dc2..b0b52e95 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -18,7 +18,7 @@ (defvar coq-script-indent nil)) (defconst coq-any-command-regexp - (proof-regexp-alt (proof-ids-to-regexp coq-keywords))) + (proof-regexp-alt-list coq-keywords)) (defconst coq-indent-inner-regexp (proof-regexp-alt @@ -35,28 +35,27 @@ (defconst coq-comment-start-or-end-regexp (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) (defconst coq-indent-open-regexp - (proof-regexp-alt ;(proof-ids-to-regexp coq-keywords-goal) goal-command-p instead + (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead (proof-ids-to-regexp '("Cases" "match")) "\\s(")) (defconst coq-indent-close-regexp - (proof-regexp-alt (proof-ids-to-regexp coq-keywords-save) - (proof-ids-to-regexp '("end" "End")) - "\\s)")) + (proof-regexp-alt-list (append coq-keywords-save '("end" "End" "\\s)")))) (defconst coq-indent-closepar-regexp "\\s)") (defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end"))) (defconst coq-indent-openpar-regexp "\\s(") (defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases"))) +(defconst coq-tacticals-tactics-regex + (proof-regexp-alt (proof-regexp-alt-list (append coq-tacticals coq-tactics)))) (defconst coq-indent-any-regexp (proof-regexp-alt coq-indent-close-regexp coq-indent-open-regexp coq-indent-inner-regexp coq-any-command-regexp - (proof-ids-to-regexp coq-tacticals) - (proof-ids-to-regexp coq-tactics))) + coq-tacticals-tactics-regex)) (defconst coq-indent-kw - (proof-regexp-alt coq-any-command-regexp coq-indent-inner-regexp - (proof-ids-to-regexp coq-tacticals) - (proof-ids-to-regexp coq-tactics))) + (proof-regexp-alt-list (cons coq-any-command-regexp + (cons coq-indent-inner-regexp + (append coq-tacticals coq-tactics))))) ; pattern matching detection, will be tested only at beginning of a ; line (only white sapces before "|") must not match "|" followed by @@ -561,7 +560,7 @@ argument must be t if inside the {}s of a record, nil otherwise." (cond ((proof-looking-at-safe "\\s(") (+ (current-indentation) proof-indent)) - ((proof-looking-at-safe (proof-ids-to-regexp coq-keywords-defn)) + ((proof-looking-at-safe (proof-regexp-alt-list coq-keywords-defn)) (current-column)) (t (+ (current-column) proof-indent))))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c0076e6a..e8ec3c12 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -10,6 +10,15 @@ (require 'proof-utils) ; proof-locate-executable (require 'coq-db) +(defsubst proof-regexp-alt-list (args) + "Return the regexp which matches any of the regexps ARGS." + ;; see regexp-opt (NB: but that is for strings, not regexps) + (let ((res "")) + (dolist (regexp args) + (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:") + regexp "\\)"))) + (concat "\\_<\\(?:"res"\\)\\_>"))) + (eval-when-compile (require 'span) (defvar coq-goal-command-regexp nil) @@ -357,6 +366,8 @@ See also `coq-prog-env' to adjust the environment." (defvar coq-decl-db '( ("Axiom" "ax" "Axiom # : #" t "Axiom") + ("Global Variable" "gv" "Global Variable #: #." t "Global\\s-+Variable") + ("Global Variables" "gvs" "Global Variables # , #: #." t "Global\\s-+Variables") ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") @@ -504,10 +515,13 @@ See also `coq-prog-env' to adjust the environment." ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") ("Focus" nil "Focus #." nil "Focus") + ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables") + ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") + ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types") ("Import" nil "Import #." t "Import") ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") ("Inspect" nil "Inspect #." nil "Inspect") @@ -562,6 +576,7 @@ See also `coq-prog-env' to adjust the environment." ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") ("Show" nil "Show #." nil "Show") ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") + ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation") ("Test" nil "Test" nil "Test" nil t) ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") @@ -883,6 +898,7 @@ Used by `coq-goal-command-p'" ; (list 0 font-lock-variable-name-face))) ;; parenthesized binders (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) )) "*Font-lock table for Coq terms.") @@ -893,33 +909,35 @@ Used by `coq-goal-command-p'" ;; recognizing global identifiers, see coq-global-p. (defconst coq-save-command-regexp-strict (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save-strict) "\\)"))) + + (defconst coq-save-command-regexp (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save) "\\)"))) (defconst coq-save-with-hole-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save-strict) "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) (defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) + (proof-anchor-regexp (proof-regexp-alt-list coq-keywords-goal))) (defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) + (concat "\\(" (proof-regexp-alt-list coq-keywords-goal) "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) (defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) + (concat "\\(" (proof-regexp-alt-list coq-keywords-decl) "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) ;; (defconst coq-decl-with-hole-regexp ;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) (defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) + (concat "\\(" (proof-regexp-alt-list coq-keywords-defn) "\\)\\s-+\\(" coq-id "\\)")) ;; must match: @@ -947,13 +965,13 @@ Group number 1 matches the name of the library which is required.") (append coq-font-lock-terms (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-solve-cheat-tactics) 'coq-cheat-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) + (cons (proof-regexp-alt-list coq-solve-tactics) 'coq-solve-tactics-face) + (cons (proof-regexp-alt-list coq-solve-cheat-tactics) 'coq-cheat-face) + (cons (proof-regexp-alt-list coq-keywords) 'font-lock-keyword-face) + (cons (proof-regexp-alt-list coq-reserved) 'font-lock-type-face) + (cons (proof-regexp-alt-list coq-tactics ) 'proof-tactics-name-face) + (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face) + (cons (proof-regexp-alt-list (list "Set" "Type" "Prop")) 'font-lock-type-face) (cons "============================" 'font-lock-keyword-face) (cons "Subtree proved!" 'font-lock-keyword-face) (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) @@ -161,17 +161,17 @@ On Windows you might need something like: ;; some of them must kept when v8.1 because they are used by state preserving ;; check when C-c C-v (defconst coq-state-preserving-tactics-regexp - (proof-ids-to-regexp coq-state-preserving-tactics)) + (proof-regexp-alt-list coq-state-preserving-tactics)) (defconst coq-state-changing-commands-regexp - (proof-ids-to-regexp coq-keywords-state-changing-commands)) + (proof-regexp-alt-list coq-keywords-state-changing-commands)) (defconst coq-state-preserving-commands-regexp - (proof-ids-to-regexp coq-keywords-state-preserving-commands)) + (proof-regexp-alt-list coq-keywords-state-preserving-commands)) (defconst coq-commands-regexp - (proof-ids-to-regexp coq-keywords-commands)) + (proof-regexp-alt-list coq-keywords-commands)) (defvar coq-retractable-instruct-regexp - (proof-ids-to-regexp coq-retractable-instruct)) + (proof-regexp-alt-list coq-retractable-instruct)) (defvar coq-non-retractable-instruct-regexp - (proof-ids-to-regexp coq-non-retractable-instruct)) + (proof-regexp-alt-list coq-non-retractable-instruct)) ;; ;; Derived modes - define keymaps |