Towards isabelle-refresh-logics

1 files changed, 23 insertions, 3 deletions

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 5068877c..3b679d34 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -240,6 +240,14 @@ Called with one argument: t to save database, nil otherwise."
 
 ;;; ==========  Utility functions ==========
 
+(defcustom isabelle-refresh-logics t
+  "*Whether to refresh the list of logics during an interactive session.
+If non-nil, then `isatool findlogics' will be used to regenerate
+the `isabelle-logics-available' setting.  If this tool does not work
+for you, you should disable this behaviour."
+  :type 'boolean
+  :group 'isabelle)
+
 (defcustom isabelle-logics-available (isa-tool-list-logics)
   "*List of logics available to use with Isabelle.
 If the `isatool' program is available, this is automatically
@@ -284,12 +292,24 @@ until Proof General is restarted."
 			   :selected (list 'equal 'isabelle-chosen-logic l)))
 		 (isa-tool-list-logics)))))
 
+;; Status: remove-menu-item 
 (defun isabelle-logics-menu-refresh ()
   "Refresh isabelle-logics-menu."
   (interactive)
-  (setq isabelle-logics-menu (isabelle-logics-menu-calculate))
-  ;; FIXME: need to do some easy-menu magic here
-  )
+  (if isabelle-refresh-logics
+      (progn
+	(setq isabelle-logics-available (isa-tool-list-logics))
+	(setq isabelle-logics-menu (isabelle-logics-menu-calculate))
+	;;(easy-menu-remove-item proof-assistant-menu
+	;;		       (list (car proof-assistant-menu))
+	;;		       "Logics")
+	(easy-menu-add-item 
+	 proof-assistant-menu 
+	 nil ;; NB: nil doesn't work: buggy or other reason?
+	 ;; Frustrating.  A workaround was found at great effort in
+	 ;; proof-menu.el for the favourites.
+	 isabelle-logics-menu))))
+
 
 (defconst isabelle-logics-menu (isabelle-logics-menu-calculate)
   "Isabelle logics menu.  Calculated when Proof General is loaded.")