diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-02-03 18:03:48 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-02-03 18:03:48 +0000 |
| commit | c19b4a336325571fc6748b4d110b43ec1045eef3 (patch) | |
| tree | 5699a2f758331068792f2727e0046d1dd361bac9 /coq/coq-syntax.el | |
| parent | caf5634f5ea3426588ad9df0b6ffdb751cbf4610 (diff) | |
coloring names in resposne and goals
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 8 |
1 files changed, 8 insertions, 0 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 () |