From 3817b477032a4fc82dd9df9b6e26c82ca77106e8 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 5 Sep 2006 14:01:27 +0000
Subject: still experimenting error highliting

---
 coq/coq.el | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 1fc5f380..b3f91827 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1401,13 +1401,17 @@ be asked to the user."
            (lgth (length (match-string 2))))
 ;    (message "pos = %d ; lgth = %d " pos lgth)
       (goto-char (+ (proof-locked-end) 1))
+      (coq-find-real-start)
       (forward-char pos)
-      (push-mark (+ (point)lgth) t t)
-      )))
+      (let ((sp (make-span (point) (+ (point) lgth))))
+        (set-span-face sp 'proof-mouse-highlight-face)
+        (sit-for 20)
+        (delete-span sp)
+        ))))
 
 ; does not show the region from there, something must be deactivating the
 ; region before going out...
-;(setq proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error)
+(setq proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error)
 
 ;(add-hook 'proof-shell-handle-error 
 ;          'zmacs-region-stays
-- 
cgit v1.2.3