aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 11:07:17 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 11:07:17 +0000
commit0ff03ffd23f25f8d84153822be1d92dc13f3ab19 (patch)
treeb87dd076c92f1ad45c6a27f2837e76c08cdb8d1b /generic
parent7b62c3c51add92fc482c4c72526377deb667df23 (diff)
Fix for deferred loading of maths menu and unicode tokens.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-auxmodes.el10
-rw-r--r--generic/proof-menu.el10
2 files changed, 10 insertions, 10 deletions
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index d204154f..69dc0b72 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -43,13 +43,9 @@
;; Maths menu
;;
(defun proof-maths-menu-support-available ()
- "A test to see whether maths-menu support is available."
- (and
- (or (featurep 'maths-menu)
- ;; *should* always succeed unless bundled version broken
- (proof-try-require 'maths-menu))
- ;; Load any optional prover-specific config in <foo>-maths-menu.el
- (or (proof-try-require (proof-ass-sym maths-menu)) t)))
+ "A test to see whether maths-menu support is available.
+The test loads optional prover-specific config in <foo>-maths-menu.el"
+ (or (proof-try-require (proof-ass-sym maths-menu)) t))
(proof-eval-when-ready-for-assistant
(if (and (proof-ass maths-menu-enable)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index b3504701..0a80beef 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -306,15 +306,19 @@ without adjusting window layout."
:help "Do not allow editing in processed region"]
["Unicode Tokens"
- (progn
- (proof-unicode-tokens-toggle (if unicode-tokens-mode 0 1)))
+ (proof-unicode-tokens-toggle (if (boundp 'unicode-tokens-mode)
+ (if unicode-tokens-mode 0 1)
+ t))
:active (proof-unicode-tokens-support-available)
:style toggle
:selected (and (boundp 'unicode-tokens-mode)
unicode-tokens-mode)
:help "Enable display of tokens as Unicode characters"]
- ["Unicode Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
+ ["Unicode Maths Menu"
+ (proof-maths-menu-toggle (if (boundp 'maths-menu-mode)
+ (if maths-menu-mode 0 1)
+ t))
:active (proof-maths-menu-support-available)
:style toggle
:selected (and (boundp 'maths-menu-mode) maths-menu-mode)