diff options
| -rw-r--r-- | coq/coq.el | 26 |
1 files changed, 26 insertions, 0 deletions
@@ -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) |