diff options
| author | David Aspinall | 1998-09-11 12:33:28 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-09-11 12:33:28 +0000 |
| commit | 28f7dadc066a7eb10389582be8372fb2ba3fb06f (patch) | |
| tree | 535f0aa9bc5920382f72f059e0581238d9e4090f /isa/isa-syntax.el | |
| parent | 7cc5edd11befabbb02610aa90a95d641ba4c00db (diff) | |
Fixes to syntax and startup function.
Diffstat (limited to 'isa/isa-syntax.el')
| -rw-r--r-- | isa/isa-syntax.el | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 52e2ee90..e01104b7 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -45,8 +45,9 @@ :group 'isa-settings) (defcustom isa-keywords-decl - '("val") - "Isabelle keywords for declarations" + '("val" "fun" "datatype" + "signature" "structure") + "Isabelle keywords for declarations. Includes ML keywords to fontify ML files." :group 'isa-syntax :type '(repeat string)) @@ -83,15 +84,17 @@ ;; See isa-command-table in Isamode/isa-menus.el to get this list. ;; BUT: tactics are not commands, so appear inside some expression. -(defvar isa-tactics +(defconst isa-tactics '("resolve_tac" "assume_tac")) -(defvar isa-keywords +;; NB: this means that any adjustments above by customize will +;; only have effect in next session. +(defconst isa-keywords (append isa-keywords-goal isa-keywords-save isa-keywords-decl isa-keywords-defn isa-keywords-commands isa-tactics) "All keywords in a Isabelle script") -(defvar isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY")) +(defconst isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY")) ;; ----- regular expressions @@ -102,9 +105,9 @@ :type 'string :group 'isa-syntax) -(defvar isa-id proof-id) +(defconst isa-id proof-id) -(defvar isa-ids (proof-ids isa-id)) +(defconst isa-ids (proof-ids isa-id)) (defun isa-abstr-regexp (paren char) (concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char)) |