diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 13:37:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 13:37:50 +0000 |
| commit | 5205d2df95632ff2801ed416c0d3484ce6ec2e11 (patch) | |
| tree | 023ab7ab78083377ffabce12d29278cbf6b16e2f /coq/coq-syntax.el | |
| parent | 5f74f36621d54ae4ba3ec4b24bb5133cbc4f4119 (diff) | |
More decoration
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c323f83e..049f9f53 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -300,7 +300,13 @@ (cons (proof-ids-to-regexp coq-tactics) 'proof-tactics-name-face) (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - + (cons "============================" 'font-lock-keyword-face) + (cons "Subtree proved!" 'font-lock-keyword-face) + (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) + (list "^\\([^ \n]+\\) \\(is defined\\)" + (list 2 'font-lock-keyword-face t) + (list 1 'font-lock-function-name-face t)) + (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face) (list coq-decl-with-hole-regexp 2 'proof-declaration-name-face) (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) |