diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-02-05 18:15:38 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-02-05 18:15:38 +0000 |
| commit | 5e83d669e5a296477f0cac85cb90d34a75116857 (patch) | |
| tree | 77435c92a0c3c0ec6d085b0cd1a286cdb716dead /coq/coq-syntax.el | |
| parent | 1d41c893d257b67211cbb99b7c1d2756141d464a (diff) | |
Fix colorization of for coq multiple hypothesis on the same line.
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 137062eb..7848bcac 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1058,7 +1058,8 @@ 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) + ;; ", " is for multiple hypothesis diplayed in v8.5. + (cons "^ *\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) @@ -1066,7 +1067,7 @@ It is used: (append coq-font-lock-terms (list - (cons "^ *[^ \n:()=]+ *:" 'proof-declaration-name-face) + (cons "^ *\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) |