Leave packages' own hooks (X-Symbol, MMM) to deal with turning on or

off minor modes in buffers automatically.  Now the PG setting controls
the "default global for PG buffers" for each of these.  The menu
checkbox simply displays the current minor mode status.  When this
is changed, the PG global mode follows suit.  We do not try to
apply the change to all PG buffers (30 minutes of fontification!).

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))))