emacs-elpa-diffs
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[nongnu] elpa/proof-general 2361fe8 1/5: Fix #597; ProofGeneral cannot s


From: ELPA Syncer
Subject: [nongnu] elpa/proof-general 2361fe8 1/5: Fix #597; ProofGeneral cannot step over `Fail` correctly
Date: Wed, 13 Oct 2021 15:57:54 -0400 (EDT)

branch: elpa/proof-general
commit 2361fe8b00016e025fe5da12cea0344564364b07
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]