diff options
| -rw-r--r-- | coq/coq-syntax.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 8 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 7cae3a88..2801ddbe 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1210,8 +1210,14 @@ It is used: (defvar coq-error-regexp "^\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" "A regexp indicating that the Coq process has identified an error.") +;; april2017: coq-8.7 removes special chars definitely and puts +;; <infomsg> and <warning> around all messages except errors. +;; We let our legacy regexp for some years and remove them, say, in 2020. (defvar coq-shell-eager-annotation-start - "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>") + "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>\\<warning>") + +(defvar coq-shell-eager-annotation-end + "\377\\|done\\]\\|</infomsg>\\|</warning>\\|\\*\\*\\*\\*\\*\\*\\|) >") (defvar coq-id "\\(@\\|_\\|\\w\\)\\(\\w\\|\\s_\\)*") ;; Coq ca start an id with @ or _ (defvar coq-id-shy "\\(?:@\\|_\\|\\w\\)\\(?:\\w\\|\\s_\\)*") @@ -1675,7 +1675,7 @@ Near here means PT is either inside or just aside of a comment." ;; 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\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done + proof-shell-eager-annotation-end coq-shell-eager-annotation-end ; 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" |