branch: elpa/proof-general
commit 2361fe8b00016e025fe5da12cea0344564364b07
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Fix #597; ProofGeneral cannot step over `Fail` correctly
The bug happened when `Set Ltac Backtrace` is enabled, which has
become the default since a few versions. The fix is to prefix the
coq-error-message variable with a negative regexp for "message:\n".
This PR should be accepted if it does not slow performances too much.
---
coq/coq-syntax.el | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b8b498a..a2266db 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1282,7 +1282,7 @@ different."
(defvar coq-symbols-regexp (regexp-opt coq-symbols))
;; ----- regular expressions
-(defvar coq-error-regexp "^\\(In nested Ltac call\\|Error:\\|Discarding
pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User
error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
+(defvar coq-error-regexp
"\\(?:[^:]\\|[^e]:\\|[^g]e:\\|[^a]ge:\\|[^s]age:\\|[^s]sage:\\|[^e]ssage:\\|[^m]essage:\\)\n\\(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
