diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
3 files changed, 14 insertions, 1 deletions
@@ -101,6 +101,11 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Support for prettify-symbols-mode. +*** Colors in response and goals buffers + + Experimental: colorize hypothesis names and some parts of error + and warning messages. For readability. + * Changes of Proof General 4.2 from Proof General 4.1 ** Generic/misc changes 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 () @@ -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 () |