diff options
| -rw-r--r-- | generic/proof-maths-menu.el | 19 | ||||
| -rw-r--r-- | generic/proof-mmm.el | 59 | ||||
| -rw-r--r-- | generic/proof-shell.el | 6 | ||||
| -rw-r--r-- | generic/proof-unicode-tokens.el | 27 | ||||
| -rw-r--r-- | generic/proof.el | 1 |
5 files changed, 24 insertions, 88 deletions
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el index 8364d711..07030623 100644 --- a/generic/proof-maths-menu.el +++ b/generic/proof-maths-menu.el @@ -28,17 +28,6 @@ ;;;###autoload -(defun proof-maths-menu-support-available () - "A test to see whether maths-menu support is available." - (and - (not (featurep 'xemacs)) ;; not XEmacs compatible - (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))) - - (defun proof-maths-menu-set-global (flag) "Set global status of maths-menu mode for PG buffers to be FLAG. Turn on/off menu in all script buffers and ensure new buffers follow suit." @@ -63,13 +52,5 @@ in future if we have just activated it for this buffer." (if (proof-maths-menu-support-available) ;; will load maths-menu-mode (proof-maths-menu-set-global (not maths-menu-mode)))) -;; -;; On start up, adjust automode according to user setting -;; -(proof-eval-when-ready-for-assistant - (if (and (proof-ass maths-menu-enable) - (proof-maths-menu-support-available)) - (proof-maths-menu-set-global t))) - (provide 'proof-maths-menu) ;; End of proof-maths-menu.el diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el index d726b731..b1ebf9e7 100644 --- a/generic/proof-mmm.el +++ b/generic/proof-mmm.el @@ -1,4 +1,4 @@ -;; proof-mmm.el Support for MMM mode package +;; proof-mmm.el --- Support for MMM mode package ;; ;; Copyright (C) 2003 LFCS Edinburgh / David Aspinall ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> @@ -6,7 +6,7 @@ ;; ;; The MMM package is at http://mmm-mode.sourceforge.net/ ;; -;; With thanks to Stefan Monnier for pointing me to this package, +;; With thanks to Stefan Monnier for pointing me to this package, ;; and Michael Abraham Shulman for providing it. ;; ;; $Id$ @@ -30,31 +30,14 @@ (require 'proof-site) -;;;###autoload -(defun proof-mmm-support-available () - "A test to see whether mmm support is available." - (and - (or (featurep 'mmm-auto) - (progn - ;; put bundled version on load path - (setq load-path - (cons - (concat proof-home-directory "mmm/") - load-path)) - ;; *should* always succeed unless bundled version broken - (proof-try-require 'mmm-auto))) - ;; Load prover-specific config in <foo>-mmm.el - (proof-try-require (proof-ass-sym mmm)))) - - -;; The following function is called by the menu item for -;; MMM-Mode. It is an attempt at an intuitive behaviour -;; without confusing the user with extra "in this buffer" -;; and "everywhere" options. We simply make the global -;; option track the last setting made for any buffer. -;; The menu toggle displays the status of the buffer -;; (as seen in the modeline) rather than the PG setting. +;; The following function is called by the menu item for MMM-Mode. It +;; is an attempt at an intuitive behaviour without confusing the user +;; with extra "in this buffer" and "everywhere" options. We make the +;; global option track the last setting made for any buffer. The menu +;; toggle displays the status of the buffer (as seen in the modeline) +;; rather than the PG setting. +;;;###autoload (defun proof-mmm-set-global (flag) "Set global status of MMM mode for PG buffers to be FLAG." (let ((automode-entry (list (proof-ass-sym mode) nil @@ -74,24 +57,16 @@ "Turn on or off MMM mode in Proof General script buffer. This invokes `mmm-mode' to toggle the setting for the current buffer, and then sets PG's option for default to match. -Also we arrange to have MMM mode turn itself on automatically +Also we arrange to have MMM mode turn itself on automatically in future if we have just activated it for this buffer." (interactive) - (if (proof-mmm-support-available) ;; will load mmm-mode - (progn - ;; Make sure auto mode follows PG's global setting. (NB: might - ;; do this only if global state changes, but by the time we - ;; get here, (proof-ass mmm-mode) has been set. - (proof-mmm-set-global (not mmm-mode)) - (mmm-mode)))) + (when (proof-mmm-support-available) + ;; Make sure auto mode follows PG's global setting. (NB: might do + ;; only if global state changes, but by now (proof-ass mmm-mode) set). + (proof-mmm-set-global (not mmm-mode)) + (mmm-mode))) -;; -;; On start up, adjust automode according to user setting -;; -(proof-eval-when-ready-for-assistant - (if (and (proof-ass mmm-enable) - (proof-mmm-support-available)) - (proof-mmm-set-global t))) (provide 'proof-mmm) -;; End of proof-mmm.el + +;;; proof-mmm.el ends here diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8d6545bd..20117797 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -870,9 +870,11 @@ which see." ;; Low-level commands for shell communication ;; -(defvar proof-shell-insert-space-fudge +(defconst proof-shell-insert-space-fudge (cond - ((string-match "21.*XEmacs" emacs-version) " ") + ((and (featurep 'xemacs) + (string-match "21.*XEmacs" emacs-version)) + " ") ((featurep 'xemacs) "") (t " ")) "String to insert after setting proof marker to prevent it moving. diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el index 7dd73bc8..50cef1c2 100644 --- a/generic/proof-unicode-tokens.el +++ b/generic/proof-unicode-tokens.el @@ -12,19 +12,7 @@ (require 'cl)) (eval-when (compile) -; (if (not (featurep 'xemacs)) - (require 'unicode-tokens)) ; it's loaded dynamically at runtime - - -;;;###autoload -(defun proof-unicode-tokens-support-available () - "A test to see whether unicode tokens support is available." - (and - ;(not (featurep 'xemacs)) ;; not XEmacs compatible - (or (featurep 'unicode-tokens) - (proof-try-require 'unicode-tokens)) - ;; Requires prover-specific config in <foo>-unicode-tokens.el - (proof-try-require (proof-ass-sym unicode-tokens)))) + (require 'unicode-tokens)) ; it's loaded dynamically at runtime (defvar proof-unicode-tokens-initialised nil "Flag indicating whether or not we've performed startup.") @@ -51,6 +39,7 @@ (unicode-tokens-initialise) (setq proof-unicode-tokens-initialised t)) +;;;###autoload (defun proof-unicode-tokens-set-global (flag) "Set global status of unicode tokens mode for PG buffers to be FLAG. Turn on/off menu in all script buffers and ensure new buffers follow suit." @@ -145,17 +134,5 @@ A value for proof-shell-insert-hook." (setq string (buffer-substring-no-properties (point-min) (point-max)))))) - - - - -;; -;; On start up, adjust automode according to user setting -;; -(proof-eval-when-ready-for-assistant - (if (and (proof-ass unicode-tokens-enable) - (proof-unicode-tokens-support-available)) - (proof-unicode-tokens-set-global t))) - (provide 'proof-unicode-tokens) ;; End of proof-unicode-tokens.el diff --git a/generic/proof.el b/generic/proof.el index 7957177b..3db52db6 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -27,6 +27,7 @@ (require 'proof-compat) ; Emacs and OS compatibility (require 'proof-utils) ; utilities (require 'proof-config) ; configuration variables +(require 'proof-auxmodes) ; further autoloads (proof-splash-message) ; welcome the user now. |