diff options
| -rw-r--r-- | isa/isabelle-system.el | 27 |
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 ======== |