diff options
| author | Patrick Loiseleur | 1999-04-20 17:12:34 +0000 |
|---|---|---|
| committer | Patrick Loiseleur | 1999-04-20 17:12:34 +0000 |
| commit | 6d1e73f779463872f89b9c0a27b0670898bbd9a8 (patch) | |
| tree | f186c6782bce178d8f4a29b4260923f60617cda8 | |
| parent | 9bafbd1b551c9cf8d7c3a7fb96511966ed094831 (diff) | |
A few coloring tricks
| -rw-r--r-- | coq/coq-syntax.el | 53 |
1 files changed, 44 insertions, 9 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index f9c1c8db..804de46f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -155,14 +155,48 @@ coq-keywords-defn coq-keywords-commands coq-tactics) "All keywords in a Coq script") -(defvar coq-tacticals '( -"Abstract" -"Do" -"Idtac" -"OrElse" -"Repeat" -"Try" -)) +(defvar coq-tacticals + '( + "Abstract" + "Do" + "Idtac" + "OrElse" + "Repeat" + "Try") + "Keywords for tacticals in a Coq script") + +(defvar coq-reserved + '( + "ALL" + "Cases" + "EX" + "else" + "end" + "Fix" + "if" + "then" + ) + "Reserved keyworkds of Coq") + + +(defvar coq-symbols + '( + "|" + ":" + ";" + "," + "(" + ")" + "[" + "]" + "{" + "}" + ":=" + "=>" + "->" + "." + ) + "Punctuation Symbols used by Coq") ;; ----- regular expressions (defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\)" @@ -216,7 +250,8 @@ (list (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - + (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) + (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) |