Fixes to syntax and startup function.

2 files changed, 13 insertions, 8 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))
diff --git a/isa/isa.el b/isa/isa.el
index f4c0a0fe..f9fc6b32 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -105,7 +105,9 @@ no regular or easily discernable structure."
    ;; initial command configures Isabelle by hacking print functions.
    ;; may need to set directory somewhere for this:
    ;; /home/da/devel/lego/elisp/   or  $PROOFGENERIC_HOME ?
-   proof-shell-init-cmd			"use \"isa-print-functions.ML\";"
+   proof-shell-init-cmd			(concat
+					 "use \"" proof-home
+					  "isa/isa-print-functions.ML\";")
    ;; === ANNOTATIONS  === remaining ones broken
    proof-shell-goal-char	        ?\375
    proof-shell-first-special-char	?\360