Skip to content

Commit

Permalink
Fix #597; ProofGeneral cannot step over Fail correctly
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Matafou committed Oct 11, 2021
1 parent 38ae8fd commit 2361fe8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion coq/coq-syntax.el
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 2361fe8

Please sign in to comment.