From a3f65f4af6c5138908b88a0ea8a4410775c832de Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 14 Sep 2006 08:27:43 +0000
Subject: fix a bug with error highlighting. Not sure it is ok but seems to
 work.

---
 coq/coq.el | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 23eb2c5e..feafec6b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1432,16 +1432,16 @@ buffer."
       ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer
       (set-buffer proof-response-buffer)
       (goto-char (point-max))
-      (let ((mtch (re-search-backward "\n>[^\n]+\n> \\( *\\)\\(\\^+\\)\n" nil 'dummy)))
+      (let* ((mtch (re-search-backward "\n>[^\n]+\n> \\( *\\)\\(\\^+\\)\n" nil 'dummy))
+             (pos (and mtch (length (match-string 1))))
+             (lgth (and (length (match-string 2))))
+             (res (list pos lgth)))
         ;; clean the response buffer from ultra-ugly underlined command line
         ;; parsed above. Don't kill the first \n
         (when (and clean mtch) (delete-region (+ mtch 1) (match-end 0)))
         (when mtch 
-          (let* ((pos (length (match-string 1)))
-                 (lgth (length (match-string 2)))
-                 (res (list pos lgth)))
-            (setq last-coq-error-location res)
-            res))))))
+          (setq last-coq-error-location res)
+          res)))))
 
 (defun coq-highlight-error (&optional parseresp clean)
   "Parses the last coq output looking at an error message. Highlight the text
-- 
cgit v1.2.3