diff options
| author | Pierre Courtieu | 2006-09-14 08:27:43 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-09-14 08:27:43 +0000 |
| commit | a3f65f4af6c5138908b88a0ea8a4410775c832de (patch) | |
| tree | 73ff4d147794d3475457dc866e58f6203a0c57b1 | |
| parent | a6c3b3e4023c6d870b2d6076445c42bb0b313187 (diff) | |
fix a bug with error highlighting. Not sure it is ok but seems to
work.
| -rw-r--r-- | coq/coq.el | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -1432,16 +1432,16 @@ buffer." ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer (set-buffer proof-response-buffer) (goto-char (point-max)) - (let ((mtch (re-search-backward "\n>[^\n]+\n> \\( *\\)\\(\\^+\\)\n" nil 'dummy))) + (let* ((mtch (re-search-backward "\n>[^\n]+\n> \\( *\\)\\(\\^+\\)\n" nil 'dummy)) + (pos (and mtch (length (match-string 1)))) + (lgth (and (length (match-string 2)))) + (res (list pos lgth))) ;; clean the response buffer from ultra-ugly underlined command line ;; parsed above. Don't kill the first \n (when (and clean mtch) (delete-region (+ mtch 1) (match-end 0))) (when mtch - (let* ((pos (length (match-string 1))) - (lgth (length (match-string 2))) - (res (list pos lgth))) - (setq last-coq-error-location res) - res)))))) + (setq last-coq-error-location res) + res))))) (defun coq-highlight-error (&optional parseresp clean) "Parses the last coq output looking at an error message. Highlight the text |
