From 07088a47b162ebc8b46acb53d0fc3b4e0e9d1dc6 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 5 Sep 2006 15:13:17 +0000 Subject: Error highliting in coq now works --- coq/coq.el | 38 +++++++++++++++----------------------- 1 file changed, 15 insertions(+), 23 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index b3f91827..f29d0932 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1393,29 +1393,21 @@ be asked to the user." (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)) - (coq-find-real-start) - (forward-char pos) - (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) - -;(add-hook 'proof-shell-handle-error -; 'zmacs-region-stays -; t) + "Parses the last coq output looking at an error message. put mark and point +around the text pointed by it." + (let ((mtch (string-match "> \\( *\\)\\(\\^+\\)\n" proof-shell-last-output))) + (when mtch + (let ((pos (length (match-string 1))) + (lgth (length (match-string 2)))) + (save-excursion + ;; proof-shell-handle-error-or-interrupt-hook is called from response buffer + (switch-to-buffer proof-script-buffer) + (goto-char (+ (proof-locked-end) 1)) + (coq-find-real-start) + (forward-char pos) + (push-mark (+ (point) lgth) t t)))))) + +(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error t) (provide 'coq) -- cgit v1.2.3