diff options
| -rw-r--r-- | generic/proof-autoloads.el | 12 | ||||
| -rw-r--r-- | generic/proof-menu.el | 23 | ||||
| -rw-r--r-- | generic/proof-mmm.el | 54 | ||||
| -rw-r--r-- | generic/proof-script.el | 12 | ||||
| -rw-r--r-- | generic/proof-x-symbol.el | 54 |
5 files changed, 109 insertions, 46 deletions
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index ff9b0068..ca7d1422 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -120,9 +120,8 @@ A test to see whether mmm support is available." nil nil) (autoload 'proof-mmm-enable "proof-mmm" "\ Turn on or off MMM mode in Proof General script buffers. -This invokes `mmm-mode' with appropriate setting for current -buffer, and adjusts -on MMM regions for the prover's class." nil nil) +This invokes `mmm-mode' to toggle the setting for the current +buffer, and then sets PG's option for the setting accordingly." nil nil) ;;;*** @@ -208,10 +207,13 @@ to the default toolbar." t nil) ;;;*** -;;;### (autoloads (proof-x-symbol-configure proof-x-symbol-shell-config proof-x-symbol-mode proof-x-symbol-decode-region proof-x-symbol-enable) "proof-x-symbol" "generic/proof-x-symbol.el") +;;;### (autoloads (proof-x-symbol-configure proof-x-symbol-shell-config proof-x-symbol-mode proof-x-symbol-decode-region proof-x-symbol-enable proof-x-symbol-support-maybe-available) "proof-x-symbol" "generic/proof-x-symbol.el") + +(autoload 'proof-x-symbol-support-maybe-available "proof-x-symbol" "\ +A test to see whether x-symbol support may be available." nil nil) (autoload 'proof-x-symbol-enable "proof-x-symbol" "\ -Turn on or off support for x-symbol, initializing if necessary. +Turn on or off support for X-Symbol, initializing if necessary. Calls proof-x-symbol-toggle-clean-buffers afterwards." nil nil) (autoload 'proof-x-symbol-decode-region "proof-x-symbol" "\ diff --git a/generic/proof-menu.el b/generic/proof-menu.el index c508e488..d2b62d2a 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -240,6 +240,7 @@ If in three window or multiple frame mode, display two buffers." (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle) (proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle) (proof-deftoggle proof-disappearing-proofs) + (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle) (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle) @@ -261,14 +262,14 @@ If in three window or multiple frame mode, display two buffers." :active t :style toggle :selected proof-output-fontify-enable] - ["X-Symbol" proof-x-symbol-toggle + ["X-Symbol" (proof-x-symbol-toggle (if x-symbol-mode 0 1)) :active (proof-x-symbol-support-maybe-available) :style toggle - :selected (proof-ass x-symbol-enable)] - ["Multiple modes" proof-mmm-toggle + :selected (and (boundp 'x-symbol-mode) x-symbol-mode)] ;; display minor mode flag + ["Multiple modes" (proof-mmm-toggle (if mmm-mode 0 1)) :active (proof-mmm-support-available) :style toggle - :selected (proof-ass mmm-enable)] + :selected mmm-mode] ["Toolbar" proof-toolbar-toggle ;; should really be split into :active & GNU Emacs's :visible :active (and (or (featurep 'toolbar) (featurep 'tool-bar)) @@ -329,6 +330,7 @@ If in three window or multiple frame mode, display two buffers." 'proof-disappearing-proofs 'proof-output-fontify-enable (proof-ass-sym x-symbol-enable) + (proof-ass-sym mmm-enable) 'proof-toolbar-enable ;; Display sub-menu 'proof-three-window-mode @@ -340,20 +342,27 @@ If in three window or multiple frame mode, display two buffers." 'proof-follow-mode)) (defun proof-quick-opts-changed-from-defaults-p () - ;; FIXME: would be nice to add. Custom support? + ;; NB: would be nice to add. Custom support? t) (defun proof-quick-opts-changed-from-saved-p () - ;; FIXME: would be nice to add. Custom support? + ;; NB: would be nice to add. Custom support? t) + +;; +;; We have menu items for saving options and reseting them. +;; We could just store the settings automatically (no save), +;; but then the reset option would have to change to restore +;; to manufacturer settings (rather then user-stored ones). +;; (defun proof-quick-opts-save () "Save current values of PG Options menu items using custom." (interactive) (apply 'pg-custom-save-vars (proof-quick-opts-vars))) (defun proof-quick-opts-reset () - "Reset PG Options menu to default values, using custom." + "Reset PG Options menu to default (or user-set) values, using custom." (interactive) (apply 'pg-custom-reset-vars (proof-quick-opts-vars))) diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el index 631b3ceb..c8dc61d6 100644 --- a/generic/proof-mmm.el +++ b/generic/proof-mmm.el @@ -37,24 +37,50 @@ (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. + +(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 + proof-assistant-symbol))) + (if flag + (add-to-list 'mmm-mode-ext-classes-alist + automode-entry) + (setq mmm-mode-ext-classes-alist + (delete automode-entry + mmm-mode-ext-classes-alist))) + ;; make sure MMM obeys the mmm-mode-ext-classes-alist + (unless (eq mmm-global-mode t) + (setq mmm-global-mode 'pg-use-mode-ext-classes-alist)))) + ;;;###autoload (defun proof-mmm-enable () - "Turn on or off MMM mode in Proof General script buffers. -This invokes `mmm-mode' with appropriate setting for current -buffer, and adjusts -on MMM regions for the prover's class." - (if (proof-mmm-support-available) + "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 +in future if we have just activated it for this buffer." + (interactive) + (if (proof-mmm-support-available) ;; will load mmm-mode (progn - (if (proof-ass mmm-enable) - (setq mmm-mode-ext-classes-alist - (adjoin (list (proof-ass-sym mode) nil - proof-assistant-symbol) - mmm-mode-ext-classes-alist)) - (setq mmm-mode-ext-classes-alist - (remassoc (proof-ass-sym mode) - mmm-mode-ext-classes-alist))) - (mmm-mode (if (proof-ass mmm-enable) 1))))) + ;; 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)))) +;; +;; On start up, adjust automode according to user setting +;; +(if (and (proof-ass mmm-enable) + (proof-mmm-support-available)) + (proof-mmm-set-global t)) (provide 'proof-mmm) diff --git a/generic/proof-script.el b/generic/proof-script.el index 589abe15..6247267e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -13,7 +13,8 @@ (require 'span) ; abstraction of overlays/extents (require 'pg-user) ; user-level commands (require 'proof-menu) ; menus for script mode - +(require 'proof-x-symbol) ; x-symbol (maybe put on automode list) +(require 'proof-mmm) ; mmm (ditto) ;; Nuke some byte-compiler warnings @@ -2494,15 +2495,8 @@ assistant." ;; Fontlock support. ;; ;; Assume font-lock case folding follows proof-case-fold-search - (proof-font-lock-configure-defaults 'autofontify proof-case-fold-search) + (proof-font-lock-configure-defaults 'autofontify proof-case-fold-search)) - ;; Maybe turn on x-symbol mode and MMM mode - (proof-x-symbol-mode) - ;; FIXME: slight bugginess here with MMM mode/font-lock: visiting - ;; a fresh file leaves the progress bar up. Perhaps turning - ;; on MMM here is wrong, is should happen automatically? - (proof-mmm-enable)) - diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index a405f187..2a53c558 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -38,7 +38,7 @@ (defvar proof-x-symbol-initialized nil "Non-nil if x-symbol support has been initialized.") -;;; ###autoload +;;;###autoload (defun proof-x-symbol-support-maybe-available () "A test to see whether x-symbol support may be available." (and window-system ; Not on a tty @@ -58,7 +58,9 @@ If ERROR is non-nil, give error on failure, otherwise a warning." (xs-feature (concat "x-symbol-" xs-lang-name)) (xs-feature-sym (intern xs-feature)) (error-or-warn - (lambda (str) (if error (error str) (warn str))))) + (lambda (str) + (progn + (if error (error str) (warn str)))))) ;; Check that support is provided. (cond ;; @@ -155,18 +157,42 @@ The package is available at http://x-symbol.sourceforge.net/")) ;; Finished. (setq proof-x-symbol-initialized t)))))) +(defun proof-x-symbol-set-global (enable) + "Set global status of X-Symbol mode for PG buffers to be ENABLE." + (let ((automode-entry + `(( ,(proof-ass-sym mode)) + t (quote ,(proof-ass x-symbol-language))))) + (if enable + (add-to-list 'x-symbol-auto-mode-alist + automode-entry) + (setq x-symbol-auto-mode-alist + (delete automode-entry x-symbol-auto-mode-alist))))) + ;;;###autoload (defun proof-x-symbol-enable () - "Turn on or off support for x-symbol, initializing if necessary. + "Turn on or off support for X-Symbol, initializing if necessary. Calls proof-x-symbol-toggle-clean-buffers afterwards." - (if (and (proof-ass x-symbol-enable) (not proof-x-symbol-initialized)) + (if (not proof-x-symbol-initialized) ;; Check inited (progn (set (proof-ass-sym x-symbol-enable) nil) ; assume failure! (proof-x-symbol-initialize 'giveerrors) (set (proof-ass-sym x-symbol-enable) t))) - (proof-x-symbol-mode-all-buffers) - (proof-x-symbol-toggle-clean-buffers)) + ;; 3.5: New behaviour is to just toggle for local buffer and + ;; output buffers, and try to persuade X-Symbol to follow + ;; our setting for defaults (on file loading) from now on. + (proof-x-symbol-set-global (not x-symbol-mode)) + (x-symbol-mode) + (proof-x-symbol-mode-associated-buffers)) + +;; Old behaviour for proof-x-symbol-enable was to update state in all +;; buffers --- but this can take ages if there are many buffers! +;; We also used to refresh the output, but this doesn't always work. +;; (proof-x-symbol-mode-all-buffers) +;; (proof-x-symbol-toggle-clean-buffers)) + + + (defun proof-x-symbol-toggle-clean-buffers () "Clear the response buffer and send proof-showproof-command. @@ -221,9 +247,8 @@ A value for proof-shell-insert-hook." - -(defun proof-x-symbol-mode-all-buffers () - "Activate/deactivate x-symbols in all Proof General buffers. +(defun proof-x-symbol-mode-associated-buffers () + "Activate/deactivate x-symbols in all Proof General associated buffers. A subroutine of proof-x-symbol-enable." ;; Response and goals buffer are fontified/decoded ;; manually in the code, configuration only sets @@ -234,7 +259,13 @@ A subroutine of proof-x-symbol-enable." (proof-x-symbol-configure)) ;; Shell has its own configuration (proof-with-current-buffer-if-exists proof-shell-buffer - (proof-x-symbol-shell-config)) + (proof-x-symbol-shell-config))) + + +(defun proof-x-symbol-mode-all-buffers () + "Activate/deactivate x-symbols in all Proof General buffers. +A subroutine of proof-x-symbol-enable." + (proof-x-symbol-mode-associated-buffers) ;; Script buffers are in X-Symbol's minor mode, ;; And so are any other buffers kept in the same token language (dolist (mode (cons proof-mode-for-script proof-xsym-extra-modes)) @@ -356,7 +387,8 @@ Assumes that the current buffer is the proof shell buffer." (if (proof-ass x-symbol-enable) (progn (proof-x-symbol-initialize) - (unless proof-x-symbol-initialized + (if proof-x-symbol-initialized + (proof-x-symbol-set-auto-mode t) ;; turn on in all PG buffers ;; If init failed, turn off x-symbol-enable for the session. (customize-set-variable (proof-ass-sym x-symbol-enable) nil)))) |