beautified a bit error messages.

2 files changed, 44 insertions, 13 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 74e9e937..61cb4d38 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -931,6 +931,9 @@ It is used:
 (defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
   "A regexp indicating that the Coq process has identified an error.")
 
+(defvar coq-shell-eager-annotation-start
+   "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>")
+
 (defvar coq-id proof-id)
 (defvar coq-id-shy "@?\\(?:\\w\\|\\s_\\)+")
 
@@ -1034,12 +1037,6 @@ It is used:
     (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face)
     (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)
     (cons "============================" 'font-lock-keyword-face)
-    (cons "Subtree proved!" 'font-lock-keyword-face)
-    (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face)
-    (list "^\\([^ \n]+\\) \\(is defined\\)"
-          (list 2 'font-lock-keyword-face t)
-          (list 1 'font-lock-function-name-face t))
-
     (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face))
     (if coq-variable-highlight-enable
         (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)))
@@ -1049,7 +1046,22 @@ It is used:
     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
     ;; Remove spurious variable and function faces on commas.
     '(proof-zap-commas))))
-(defvar coq-font-lock-keywords coq-font-lock-keywords-1)
+
+;; We define a slightly different set of keywords for response buffer.
+
+(defvar coq-response-font-lock-keywords
+   (append
+    coq-font-lock-terms
+    (list
+     (cons coq-keywords-regexp 'font-lock-keyword-face)
+     (cons coq-shell-eager-annotation-start 'proof-warning-face)
+     (cons coq-error-regexp 'proof-error-face)
+     (cons (proof-regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face)
+     (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)
+     (list "^\\([^ \n]+\\) \\(is defined\\)"
+           (list 1 'font-lock-function-name-face t)))))
+
+
 
 (defun coq-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
diff --git a/coq/coq.el b/coq/coq.el
index 601795e7..08be0321 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -384,8 +384,29 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3."
        (str (proof-shell-strip-eager-annotations start end))
        (strnotrailingspace
         (coq-remove-starting-blanks (coq-remove-trailing-blanks str))))
-    (pg-response-display-with-face strnotrailingspace face)))
-
+    (pg-response-display-with-face strnotrailingspace))) ; face
+
+
+(defun proof-shell-handle-error-output (start-regexp append-face)
+"A replacement fo `proof-shell-handle-error-output' for Coq.
+No global coloring of the error with error-face
++ removes useless location."
+  (let ((string proof-shell-last-output) pos)
+    (if (and start-regexp
+             (setq pos (string-match start-regexp string)))
+        (setq string (substring string pos)))
+
+    ;; Erase if need be, and erase next time round too.
+    (pg-response-maybe-erase t nil)
+    (pg-response-display-with-face string) ;removed this:append-face
+    ;; first highlight the error regexp in response buffer
+    (proof-with-current-buffer-if-exists proof-response-buffer
+      ;; remove location TODO: put this in coq-highlight-error?
+      (goto-char (point-min))
+      (when (looking-at "Toplevel input[^:]+:")
+        (let ((inhibit-read-only t))
+          (kill-line 1)
+          (setq kill-ring (cdr kill-ring)))))))
 
 
 ;;;;;;;;;;; Trying to accept { and } as terminator for empty commands. Actually
@@ -1473,8 +1494,7 @@ Warning:
 
    ;; FIXME: ideally, the eager annotation should just be a single "special" char,
    ;; this requires changes in Coq.
-   proof-shell-eager-annotation-start 
-   "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>"
+   proof-shell-eager-annotation-start coq-shell-eager-annotation-start
    proof-shell-eager-annotation-start-length 32
 
    proof-shell-interactive-prompt-regexp "TcDebug "
@@ -1556,12 +1576,11 @@ Warning:
 
 (defun coq-response-config ()
   (coq-init-syntax-table)
-  (setq proof-response-font-lock-keywords coq-font-lock-keywords-1)
+  (setq proof-response-font-lock-keywords coq-response-font-lock-keywords)
   ;; The line wrapping in this buffer just seems to make it less readable.
   (setq truncate-lines t)
   (proof-response-config-done))
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Flags and other settings for Coq.