Added isabelle-load-isar-keywords mimic of script startup.

1 files changed, 25 insertions, 2 deletions

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index d48de66e..6ca185c7 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -11,9 +11,11 @@
 ;; --------------------------------------------------------------
 ;;
 
-(require 'proof)
+(require 'proof)			; for proof-assistant-symbol, etc.
+(require 'proof-syntax)			; for proof-string-match
 
-(defconst isa-running-isar (eq proof-assistant-symbol 'isar))
+(defconst isa-running-isar 
+  (eq proof-assistant-symbol 'isar))
 
 ;; If we're using Isabelle/Isar then the isabelle custom
 ;; group won't have been defined yet.
@@ -265,6 +267,27 @@ until Proof General is restarted."
   "Isabelle logics menu.  Constructed when PG is loaded.")
 
 
+;; Added in PG 3.4: load isar-keywords file.
+;; This roughly follows the method given in the interface script.
+;; It could be used to add an elisp command at the bottom of
+;; a theory file, if we sorted out the load order a bit, or
+;; added a facility to reconfigure.
+;; TODO: also add something to spill out a keywords file?
+(defun isabelle-load-isar-keywords (&optional kw)
+  (interactive "Load isar keywords: %s")
+  (let ((userhome  (isa-getenv "ISABELLE_HOME_USER"))
+	(isahome   (isa-getenv "ISABELLE_HOME"))
+	(isarkwel  "%s/etc/isar-keywords-%s.el")
+	(isarel    "%s/etc/isar-keywords.el")
+	(ifrdble   (lambda (f) (if (file-readable-p f) f))))
+    (load-file
+     (or
+      (and kw (funcall ifrdble (format isarkwel userhome kw)))
+      (and kw (funcall ifrdble (format isarkwel isahome kw)))
+      (funcall ifrdble (format isarel userhome))
+      (funcall ifrdble (format isarel isahome))
+      (locate-library "isar-keywords")))))
+
 
 ;;; ========== Mirroring Proof General options in Isabelle process ========