From e76f14da4b7e737a5b6f5321c02127256d0b65df Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 5 Sep 2006 08:56:12 +0000
Subject: Experimenting highlighting the error from coqtop error message.
 Function work but proof-shell-handle-error-or-interrupt-hook does not allow
 to activate the region...

---
 coq/coq.el | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/coq/coq.el b/coq/coq.el
index d1114757..1fc5f380 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1383,9 +1383,35 @@ be asked to the user."
 (define-key coq-keymap [(control ?l)] 'coq-LocateConstant)
 (define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
 (define-key coq-keymap [(control ?g)] 'coq-Show)
+(define-key coq-keymap [?'] 'coq-highlight-error)
 
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;
+;; error handling
+;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(defun coq-highlight-error ()
+  (interactive "_")
+  (message "hook!")
+  (let ((s proof-shell-last-output))
+    (string-match "> \\( *\\)\\(\\^+\\)\n" s)
+    (let* ((pos (length (match-string 1)))
+           (lgth (length (match-string 2))))
+;    (message "pos = %d ; lgth = %d " pos lgth)
+      (goto-char (+ (proof-locked-end) 1))
+      (forward-char pos)
+      (push-mark (+ (point)lgth) t t)
+      )))
+
+; 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)
+
+;(add-hook 'proof-shell-handle-error 
+;          'zmacs-region-stays
+;          t)
 
 (provide 'coq)
 
-- 
cgit v1.2.3