diff options
| author | Healfdene Goguen | 1998-06-10 11:38:04 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1998-06-10 11:38:04 +0000 |
| commit | e9aeaece10022fe6f81e97ee3b5ebcfcd5914fe0 (patch) | |
| tree | 40fcfcdc66d5c6d7a3d4caa141b3e28ec5cf51f0 | |
| parent | 165db3d258f96567010fa74ff69528530222aea7 (diff) | |
Added "Mutual Inductive" as definition keyword.
Changed "\\s " into "\\s-" as whitespace pattern.
| -rw-r--r-- | coq-fontlock.el | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index 0a2dddf9..14fbc281 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,10 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.13 1998/06/10 11:38:04 hhg +;; Added "Mutual Inductive" as definition keyword. +;; Changed "\\s " into "\\s-" as whitespace pattern. +;; ;; Revision 1.12 1998/06/03 18:01:54 hhg ;; Changed Compute from command to tactic. ;; Added Fix, Destruct and Cofix as tactics. @@ -74,6 +78,7 @@ "CoInductive" "Fixpoint" "Inductive" +"Mutual\\s-+Inductive" )) (defvar coq-keywords-goal @@ -209,7 +214,7 @@ (defvar coq-ids (proof-ids coq-id)) (defun coq-abstr-regexp (paren char) - (concat paren "\\s *\\(" coq-ids "\\)\\s *" char)) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) (defvar coq-font-lock-terms (list @@ -221,7 +226,7 @@ (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) ;; Kinds - (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s *\\((" + (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\((" coq-id ")\\)?") 'font-lock-type-face)) "*Font-lock table for Coq terms.") |