diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-11 13:24:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-11 13:24:33 +0000 |
| commit | f86882c6352c97753f74883cfeb4f17dab8d2f34 (patch) | |
| tree | 80f4986fcb6b35963f39bace7ce82207a7e68c11 | |
| parent | 66004cbbdf3858f12482990af7b06291e676d262 (diff) | |
added proof-really-save-command-p to coq config, to deal with Proof
<term>. which is a save command (but not a save giving a name like
Save id.).
| -rw-r--r-- | coq/coq-syntax.el | 16 | ||||
| -rw-r--r-- | coq/coq.el | 1 |
2 files changed, 13 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 06b5897a..82d13924 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -230,7 +230,9 @@ of STRG matching REGEXP. Empty match are counted once." ) -(defvar coq-keywords-save + + +(defvar coq-keywords-save-strict '("Defined" "Save" "Qed" @@ -238,9 +240,13 @@ of STRG matching REGEXP. Empty match are counted once." "Admitted" )) -(defun coq-save-command-p (str) +(defvar coq-keywords-save + (append coq-keywords-save-strict '("Proof")) +) + +(defun coq-save-command-p (span str) "Decide whether argument is a Save command or not" - (or (proof-string-match coq-save-command-regexp str) + (or (proof-string-match coq-save-command-regexp-strict str) (and (proof-string-match "\\`Proof\\>" str) (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) ) @@ -735,10 +741,12 @@ Idtac (Nop) tactic, put the following line in your .emacs: ;; According to Coq, "Definition" is both a declaration and a goal. ;; It is understood here as being a goal. This is important for ;; recognizing global identifiers, see coq-global-p. +(defconst coq-save-command-regexp-strict + (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save-strict))) (defconst coq-save-command-regexp (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save))) (defconst coq-save-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-save) + (concat "\\(" (proof-ids-to-regexp coq-keywords-save-strict) "\\)\\s-+\\(" coq-id "\\)\\s-*\.")) (defconst coq-goal-command-regexp (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) @@ -758,6 +758,7 @@ This is specific to coq-mode." proof-state-preserving-p 'coq-state-preserving-p) (setq proof-save-command-regexp coq-save-command-regexp + proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>. proof-save-with-hole-regexp coq-save-with-hole-regexp proof-goal-with-hole-regexp coq-goal-with-hole-regexp proof-nested-undo-regexp coq-state-changing-commands-regexp) |