diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-11-15 13:50:51 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-11-15 13:50:51 +0000 |
| commit | 17e3598c76cb426e96b973fb49c53a4227877383 (patch) | |
| tree | 6ebb3da0beb65bd913478b2bd036435e58dbca57 /coq | |
| parent | 0d6be0aee27af7773714e2baa7ce344c11b41f53 (diff) | |
Quick stab at support for switching to proof shell when interactive support expected, see Trac #430
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -1166,14 +1166,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:" + ;; FIXME: ideally, the eager annotation should just be a single "special" char, + ;; this requires changes in Coq. + proof-shell-eager-annotation-start + "\376\\|\\[Reinterning\\|Warning:\\|TcDebug " proof-shell-eager-annotation-start-length 12 ;; ****** 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 - proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*" ; done + proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*\\|) >" ; 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" |