diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-04-07 09:04:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-04-07 09:04:33 +0000 |
| commit | c2eb2fdc71728878b019c1b87ff8cdc5d96bb00c (patch) | |
| tree | eba603baf7fa0b44b293457c7180f41b3ccbca45 /coq/coq-syntax.el | |
| parent | 7aaf6c9f278062ab6744aa036226a1c4be34d98b (diff) | |
Fixed highlighting of evars.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 14ca9c48..33f5382e 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1076,7 +1076,7 @@ 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) - (list "[?][a-zA-Z0-9]+" 0 'proof-eager-annotation-face);; highlight evars + (list (concat "[?]" proof-id) 0 'proof-eager-annotation-face);; highlight evars ;; ", " is for multiple hypothesis diplayed in v8.5. (cons "^ \\{0,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) @@ -1085,7 +1085,7 @@ It is used: (append coq-font-lock-terms (list - (list "[?][a-zA-Z0-9]+" 0 'proof-eager-annotation-face);; highlight evars + (list (concat "[?]" proof-id) 0 'proof-eager-annotation-face);; highlight evars (cons "^ \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) |