From 9e394174695f002cd55419ba0db21e44b1270ddf Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 25 Sep 2015 17:43:20 +0200 Subject: colorizing hypothesis in compact mode. --- coq/coq-syntax.el | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'coq/coq-syntax.el') diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e86d1fc9..7f518615 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1092,8 +1092,9 @@ It is used: (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 (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars - ;; ", " is for multiple hypothesis diplayed in v8.5. - (cons "^ \\{0,1,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) + ;; ", " is for multiple hypothesis diplayed in v8.5. If more than + ;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) + (cons "\\(^\\| \\) \\{0,1,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) (defvar coq-goals-font-lock-keywords @@ -1102,7 +1103,7 @@ It is used: (list (cons coq-reserved-regexp 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars - (cons "\\(^\\| *ยง\\)? \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) + (cons "\\(^\\| \\) \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) -- cgit v1.2.3