coloring names in resposne and goals

2 files changed, 9 insertions, 1 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 61cb4d38..761cc51e 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1058,9 +1058,17 @@ It is used:
      (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)
+     (cons "^[^\n:()]+:" 'proof-declaration-name-face)
      (list "^\\([^ \n]+\\) \\(is defined\\)"
            (list 1 'font-lock-function-name-face t)))))
 
+(defvar coq-goals-font-lock-keywords
+   (append
+    coq-font-lock-terms
+    (list
+     (cons "^[^\n:()]+:" 'proof-declaration-name-face)
+     (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face))))
+
 
 
 (defun coq-init-syntax-table ()
diff --git a/coq/coq.el b/coq/coq.el
index 08be0321..2f596885 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1571,7 +1571,7 @@ Warning:
   (setq pg-goals-change-goal "Show %s . ")
   (setq pg-goals-error-regexp coq-error-regexp)
   (coq-init-syntax-table)
-  (setq proof-goals-font-lock-keywords coq-font-lock-keywords-1)
+  (setq proof-goals-font-lock-keywords coq-goals-font-lock-keywords)
   (proof-goals-config-done))
 
 (defun coq-response-config ()