diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-05-29 09:50:15 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-05-29 09:50:15 +0000 |
| commit | 262093696537f2cf3d47995a2757ae7c7b6a9006 (patch) | |
| tree | 9bd05377a7fdd6d83e342f74997661cdc7ecdb57 /lego-fontlock.el | |
| parent | c10a6f6aa1e5a476dfbd990710fc5bed39a49b86 (diff) | |
o outsourced indentation to proof-indent
o support indentation of commands
o replaced test of Emacs version with availability test of specific
features
o C-c C-c, C-c C-v and M-tab is now available in all buffers
Diffstat (limited to 'lego-fontlock.el')
| -rw-r--r-- | lego-fontlock.el | 39 |
1 files changed, 27 insertions, 12 deletions
diff --git a/lego-fontlock.el b/lego-fontlock.el index 9b3ef66e..289d8328 100644 --- a/lego-fontlock.el +++ b/lego-fontlock.el @@ -3,7 +3,16 @@ ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; should perhaps be called lego-syntax instead of lego-fontlock + ;; $Log$ +;; Revision 1.5 1998/05/29 09:49:40 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; ;; Revision 1.4 1998/05/22 09:37:12 tms ;; included "Invert" in `lego-keywords' ;; @@ -28,22 +37,28 @@ ;; ----- keywords for font-lock. -(defvar lego-keywords-goal '("$?Goal")) +(defconst lego-keywords-goal '("$?Goal")) -(defvar lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) +(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) -(defvar lego-keywords +(defconst lego-commands (append lego-keywords-goal lego-keywords-save '("allE" "allI" "andE" "andI" "Assumption" "Claim" - "Constructors" "Cut" "Discharge" "DischargeKeep" - "Double" "echo" "ElimOver" "exE" "exI" "Expand" "ExpAll" - "ExportState" "Equiv" "Fields" "Freeze" "From" "Hnf" "Immed" - "impE" "impI" "Import" "Induction" "Inductive" "Inversion" - "Invert" "Init" "intros" "Intros" "Module" "Next" "NoReductions" - "Normal" "notE" "notI" "orE" "orIL" "orIR" "Parameters" "Qnify" - "Qrepl" "Record" "Refine" "Relation" "Theorems" "Unfreeze"))) - -(defvar lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) + "Cut" "Discharge" "DischargeKeep" + "echo" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" + "Normal" "notE" "notI" "orE" "orIL" "orIR" "Qnify" + "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) + "Subset of LEGO keywords and tacticals which are terminated by a \?;") + +(defconst lego-keywords + (append lego-commands + '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" + "NoReductions" "Parameters" "Relation" "Theorems"))) + +(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) ;; ----- regular expressions for font-lock (defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" |