diff options
| author | David Aspinall | 2010-09-09 17:00:35 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-09-09 17:00:35 +0000 |
| commit | 38f54757ef5363586305778d37707176c25f0245 (patch) | |
| tree | 2973edc493e3115609b3c389d9eeb4c71adca9f4 | |
| parent | 6dabc28114f0ee2ba03b79c4bdd313154cab8d30 (diff) | |
Hack regexps so that goals are cleared on Proof Completed. message. Unfortunately that message is now not shown in response buffer.
| -rw-r--r-- | coq/coq.el | 14 |
1 files changed, 9 insertions, 5 deletions
@@ -110,7 +110,7 @@ On Windows you might need something like: ;; "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists). "*Command of the inferior process to change the directory.") -(defvar coq-shell-proof-completed-regexp "Subtree\\s-proved!\\|Proof\\s-completed" +(defvar coq-shell-proof-completed-regexp "Subtree\\s-proved\\|Proof\\s-completed" "*Regular expression indicating that the proof has been completed.") (defvar coq-goal-regexp @@ -744,6 +744,7 @@ This is specific to `coq-mode'." proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-clear-goals-regexp coq-shell-proof-completed-regexp proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp + proof-shell-clear-goals-regexp coq-shell-proof-completed-regexp proof-shell-error-regexp coq-error-regexp proof-shell-interrupt-regexp coq-interrupt-regexp proof-shell-assumption-regexp coq-id @@ -754,14 +755,17 @@ This is specific to `coq-mode'." pg-subterm-end-char ?\374 ; not done pg-topterm-regexp "\375" - proof-shell-eager-annotation-start "\376\\|\\[Reinterning\\|Warning:" - proof-shell-eager-annotation-start-length 12 + proof-shell-eager-annotation-start + (concat "\376\\|\\[Reinterning\\|Warning:\\|" coq-shell-proof-completed-regexp) + proof-shell-eager-annotation-start-length 16 - ;; ****** is added at the end of warnings in emacs mode, this is temporary I + ;; ****** is added at the end of warnings in emacs mode, this is temporary. I ;; want xml like tags, and I want them removed before warning display. ;; I want the same for errors -> pgip + ;; additional hack: final ! or . matches end of coq-shell-proof-completed-regexp + ;; to get goals clearing to work with coq-shell-proof-completed-regexp - proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*" ; done + proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*\\|!\\|\\." proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" |