From 758e679ebcfce22099ba4b360b7c0ed7bee2a736 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 24 Apr 2017 11:28:59 +0200 Subject: Preparing new warning tags (no more special chars). --- coq/coq-syntax.el | 8 +++++++- coq/coq.el | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) (limited to 'coq') 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 +;; and 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 \\|") + "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|\\") + +(defvar coq-shell-eager-annotation-end + "\377\\|done\\]\\|\\|\\|\\*\\*\\*\\*\\*\\*\\|) >") (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\\]\\|\\|\\*\\*\\*\\*\\*\\*\\|) >" ; 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" -- cgit v1.2.3