diff options
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/isar/isar.el b/isar/isar.el index 6985d309..e2ddf4c2 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -239,20 +239,26 @@ See -k option for Isabelle interface script." ;;; (Settings for Isabelle are configured automatically via PGIP message) ;;; -(defun isar-configure-from-settings () - (isar-set-proof-find-theorems-command)) + +(defun isar-use-find-theorems-form-set (sym val) + (set-default sym val) + (when (featurep 'isar) ; not during loading + (isar-set-proof-find-theorems-command))) (defcustom isar-use-find-theorems-form nil "Use a form-style input for the find theorems operation." :type 'boolean :group 'isabelle - :eval (isar-set-proof-find-theorems-command)) + :set 'isar-use-find-theorems-form-set) (defun isar-set-proof-find-theorems-command () - (setq proof-find-theorems-command - (if isar-use-find-theorems-form - 'isar-find-theorems-form - 'isar-find-theorems-minibuffer))) + (setq proof-find-theorems-command + (if isar-use-find-theorems-form + 'isar-find-theorems-form + 'isar-find-theorems-minibuffer))) + +(defun isar-configure-from-settings () + (isar-set-proof-find-theorems-command)) ;;; ;;; Theory loader operations |