Preparing new warning tags (no more special chars).

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_\\)*")
diff --git a/coq/coq.el b/coq/coq.el
index d7177044..418fbb4c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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"