[nongnu] elpa/proof-general db3289d 1/2: Fix #614. Cause by 8215623.

[ELPA Syncer]

branch: elpa/proof-general
commit db3289d65fcea6fe69feb5f405fe42541f910357
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    Fix #614. Cause by 8215623.
    
    The regexp change in 8215623 to support "Fail" command had to be
    refined to capture correctly some error messages.
---
 coq/coq-syntax.el | 34 +++++++++++++++++++++++++++++++++-
 coq/coq.el        |  5 ++++-
 2 files changed, 37 insertions(+), 2 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a2266db..0ceb46f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1249,6 +1249,9 @@ different."
 (defun coq--regexp-alt-list-symb (args)
   (concat "\\_<\\(?:" (mapconcat #'identity args "\\|") "\\)\\_>"))
 
+(defun coq--regexp-alt-list (args)
+  (concat "\\(?:" (mapconcat #'identity args "\\|") "\\)"))
+
 (defvar coq-keywords-regexp (coq--regexp-alt-list-symb coq-keywords))
 
 
@@ -1281,8 +1284,37 @@ different."
 
 (defvar coq-symbols-regexp (regexp-opt coq-symbols))
 
+;; HACKISH: This string matches standard error regexp UNLESS there is
+;; the standard header of the "Fail" command (which is "The command
+;; blah has indeed failed with message:\n"). The case where the error
+;; header has nothing before it is treated using "empty string at
+;; start" regexp. BUT coq-error-regexp (and hence
+;; proof-shell-error-regexp) must be correct either when searching in
+;; a string or when searching in the proof-shell-buffer when point is
+;; at the start of the last output. Hence when we use \\` (empty
+;; string at start of the string) we should also accept \\= (empty
+;; string at point).
+(defvar coq--prefix-not-regexp 
"\\(\\(\\`\\|\\=\\)\n?\\)\\|\\(?:\\(?:[^:]\\|[^e]:\\|[^g]e:\\|[^a]ge:\\|[^s]age:\\|[^s]sage:\\|[^e]ssage:\\|[^m]essage:\\)\n\\)"
+  "A regexp matching allowed text before coq error.")
+
+(defvar coq--error-header-re-list
+  '("In nested Ltac call"
+    "Discarding pattern"
+    "Syntax error:"
+    "System Error:"
+    "User Error:"
+    "User error:"
+    "Anomaly[:.]"
+    "Toplevel input"
+    "\\<Error:")
+  "A list of regexps matching coq error headers.")
+
+(defvar coq--raw-error-regexp (coq--regexp-alt-list coq--error-header-re-list))
+
 ;; ----- regular expressions
-(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[,]\\)"
+;; ignore "Error:" if preceded by \n[ ^]+\n
+(defvar coq-error-regexp
+  (concat "\\(?:" coq--prefix-not-regexp "\\)" coq--raw-error-regexp)
   "A regexp indicating that the Coq process has identified an error.")
 
 ;; april2017: coq-8.7 removes special chars definitely and puts
diff --git a/coq/coq.el b/coq/coq.el
index a112516..99dbac8 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3021,6 +3021,9 @@ Completion is on a quasi-exhaustive list of Coq 
tacticals."
 (defvar last-coq-error-location nil
   "Last error from `coq-get-last-error-location' and `coq-highlight-error'.")
 
+(defvar coq--error-location-regexp
+  "^Toplevel input[^:]+:\n> \\(.*\\)\n> \\([^^]*\\)\\(\\^+\\)\n"
+  "A regexp to search the header of coq error locations.")
 
 ;; I don't use proof-shell-last-output here since it is not always set to the
 ;; really last output (specially when a *tactic* gives an error) instead I go
@@ -3049,7 +3052,7 @@ buffer."
     ;; then highlight the corresponding error location
     (proof-with-current-buffer-if-exists proof-response-buffer
       (goto-char (point-max)) ;\nToplevel input, character[^:]:\n
-      (when (re-search-backward "^Toplevel input[^:]+:\n> \\(.*\\)\n> 
\\([^^]*\\)\\(\\^+\\)\n" nil t)
+      (when (re-search-backward coq--error-location-regexp nil t)
         (let ((text (match-string 1))
               (pos (length (match-string 2)))
               (len (length (match-string 3))))