diff options
| author |  Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-30 15:58:33 +0000 |
|---|---|---|
| committer | Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk> | 1997-10-30 15:58:33 +0000 |
| commit | dbaa145b6a390b2febaf0cff7b3a759d6589d819 (patch) | |
| tree | 63f9675325bf3ccb1661554f25f261dcfe45d0e9 /coq-fontlock.el | |
| parent | 88c3310c6dcde027d1e70d7a0cbf711f6972d842 (diff) | |
Updates for coq, including:
* pbp-goal-command and pbp-hyp-command use proof-terminal-string
* updates to keywords
* fix for goal regexp
Diffstat (limited to 'coq-fontlock.el')
| -rw-r--r-- | coq-fontlock.el | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index b3fbfa98..8f2672c0 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,12 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.5 1997/10/30 15:58:29 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; ;; Revision 1.4 1997/10/24 14:51:07 hhg ;; Changed order of "Inversion_clear" and "Inversion" so that former is ;; fontified first. @@ -104,8 +110,11 @@ "EApply" "EAuto" "Elim" +"End" "Exact" +"Exists" "Generalize" +"Grammar" "Hnf" "Induction" "Injection" @@ -116,6 +125,7 @@ "Inversion" "LApply" "Linear" +"Load" "Pattern" "Program" "Prolog" @@ -124,10 +134,13 @@ "Reflexivity" "Replace" "Rewrite" +"Section" "Simplify_eq" "Simpl" "Specialize" +"Split" "Symmetry" +"Syntax" "Tauto" "Transitivity" "Trivial" @@ -149,7 +162,7 @@ ;; ----- regular expressions for font-lock ;; *** To update -(defvar coq-error-regexp "^\\(Error\\|Syntax error\\)" +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" "A regular expression indicating that the Coq process has identified an error.") |