diff options
| author | David Aspinall | 2005-01-28 18:39:09 +0000 |
|---|---|---|
| committer | David Aspinall | 2005-01-28 18:39:09 +0000 |
| commit | cae6a9ec9f75a34b990ff1beb59f6bd9aaaab73b (patch) | |
| tree | 09f97848963495675aaf726d3abcd94968d38f60 | |
| parent | 5099574ff152bbfa25d3fd8b673a95911fe4bfa9 (diff) | |
Patch from Stefan Monnier:
The * of (* is not quoted in the font-lock keywords leading to the
possibility of matching the empty string, which tends to put font-lock
in an infinite loop. Actually I think the infinite looping is due to a
local bug in my experimental Emacs code, but the \\ is needed in order
to really match what was intended.
| -rw-r--r-- | coq/coq-syntax.el | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 1df99654..7a5c584d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -53,7 +53,7 @@ above coq-8.0beta. To do that, put (setq coq-version-is-V8 t) in your coq-version-is-V6, coq-version-is-V7 and coq-version-is-V74. If none of these 4 variables is set to t, then ProofGeneral guesses the version of coq by doing 'coqtop -v'. If this variable is put to t -(before PG is loaded) then V74 is automatically put to t." ) +\(before PG is loaded) then V74 is automatically put to t." ) @@ -155,26 +155,25 @@ version of coq by doing 'coqtop -v'. If this variable is put to t "Ltac")) ;; Modules are like section in v > 7.4. -(if (or coq-version-is-V74 coq-version-is-V8) - (defvar coq-keywords-goal +(defvar coq-keywords-goal + (if (or coq-version-is-V74 coq-version-is-V8) '("Add\\s-+Morphism" "Chapter" - "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el) + "Declare\\s-+Module" ;;only if not followed by:=(see coq-proof-mode-p in coq.el) "Module" "Module\\s-+Type" "Section" "Correctness" - "Definition";; only if not followed by := (see coq-proof-mode-p in coq.el) + "Definition" ;; only if not followed by := (see coq-proof-mode-p in coq.el) "Fact" "Goal" "Lemma" "Local" "Remark" - "Theorem")) - (defvar coq-keywords-goal + "Theorem") '("Chapter" "Correctness" - "Definition";; only if not followed by := (see coq-proof-mode-p in coq.el) + "Definition" ;; only if not followed by := (see coq-proof-mode-p in coq.el) "Fact" "Goal" "Lemma" @@ -294,7 +293,7 @@ Print and Check commands, put the following line in your .emacs: ;; ;; Print Hint ==> state preserving (defvar coq-keywords-state-preserving-commands - (append '("(*" ;;Pierre comments must not be undone + (append '("(\\*" ;;Pierre comments must not be undone "Add\\s-+LoadPath" "Add\\s-+ML\\s-+Path" "Add\\s-+Rec\\s-+ML\\s-+Path" |