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...

1 files changed, 26 insertions, 0 deletions

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)