Reorganized user options. Special new code for boolean settings.

6 files changed, 221 insertions, 191 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2efe64af..ea1e038e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -66,6 +66,17 @@
 ;;
 ;; ==================================================
 
+
+;; Function for setting boolean values
+(defun proof-set-bool (sym value)
+  "Set a boolean customize variable using set-default and a function.
+If there is a function <blah> with the same name as the variable <blah>,
+it is called to take some action for the new setting."
+  (set-default sym value)
+  (if (fboundp sym) (funcall sym)))
+
+
+
 
 ;;
 ;; 1. User options for proof mode
@@ -80,49 +91,56 @@
   :group 'proof-general
   :prefix "proof-")
 
-(defcustom proof-prog-name-ask nil
-  "*If non-nil, query user which program to run for the inferior process."
+(defcustom proof-splash-enable t
+  "*If non-nil, display a splash screen when Proof General is loaded."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-prog-name-guess nil
-  "*If non-nil, use `proof-guess-command-line' to guess proof-prog-name.
-This option is compatible with proof-prog-name-ask.
-No effect if proof-guess-command-line is nil."
+
+(defcustom proof-electric-terminator-enable nil 
+  "*If non-nil, use electric terminator mode on start-up.
+If electric terminator mode is enabled, pressing a terminator will 
+automatically issue `proof-assert-next-command' for convenience,
+to send the command straight to the proof process.  Electric!"
   :type 'boolean
+  :set 'proof-set-bool
   :group 'proof-user-options)
 
-(defcustom proof-toolbar-inhibit nil
-  "*Non-nil prevents toolbar being used for script buffers.
+(defcustom proof-toolbar-enable t
+  "*If non-nil, display Proof General toolbar for script buffers.
 NB: the toolbar is only available with XEmacs."
   :type 'boolean
+  :set 'proof-set-bool
   :group 'proof-user-options)
 
-(defcustom proof-toolbar-use-enablers t
-  "*If non-nil, toolbars buttons may be enabled/disabled automatically.
-Toolbar buttons can be automatically enabled/disabled according to
-the context.  Set this variable to nil if you don't like this feature
-or if you find it unreliable.
-
-Notes: 
-* Toolbar enablers are only available with XEmacs 21 and later.
-* With this variable nil, buttons do nothing when they would
-otherwise be disabled.
-* If you change this variable it will only be noticed when you 
-next start Proof General."
+(defcustom proof-x-symbol-enable nil
+  "*Whether to use x-symbol in Proof General buffers.
+If you activate this variable, whether or not you get x-symbol support
+depends on if your proof assistant supports it and it is enabled
+inside your Emacs."
   :type 'boolean
+  :set 'proof-set-bool
   :group 'proof-user-options)
 
-(defcustom proof-toolbar-follow-mode 'locked
-  "*Choice of how point moves with toolbar commands.
-One of the symbols: 'locked, 'follow, 'ignore.
-If 'locked, point sticks to the end of the locked region with toolbar commands.
-If 'follow, point moves just when needed to display the locked region end.
-If 'ignore, point is never moved after toolbar movement commands."
-  :type '(choice
-	  (const :tag "Follow locked region" locked)
-	  (const :tag "Keep locked region displayed" follow)
-	  (const :tag "Never move" ignore))
+
+(defcustom proof-strict-read-only 
+  ;; For FSF Emacs, strict read only is buggy when used in
+  ;; conjunction with font-lock.
+  ;; The second conjunctive ensures that the expression is either
+  ;; `nil' or `strict' (and not 15!!).  
+  (and (string-match "XEmacs" emacs-version) 'strict)
+  "*Whether Proof General is strict about the read-only region in buffers.
+If non-nil, an error is given when an attempt is made to edit the
+read-only region.  If nil, Proof General is more relaxed (but may give
+you a reprimand!).
+
+If you change proof-strict-read-only during a session, you must use
+\"Restart\" (proof-shell-restart)
+
+The default value for proof-strict-read-only depends on which
+version of Emacs you are using.  In FSF Emacs, strict read only is buggy
+when it used in conjunction with font-lock, so it is disabled by default."
+  :type 'boolean
   :group 'proof-user-options)
 
 (defcustom proof-window-dedicated nil
@@ -149,23 +167,29 @@ experienced Emacs users."
   :type 'boolean 
   :group 'proof-user-options)
 
-(defcustom proof-strict-read-only 
-  ;; For FSF Emacs, strict read only is buggy when used in
-  ;; conjunction with font-lock.
-  ;; The second conjunctive ensures that the expression is either
-  ;; `nil' or `strict' (and not 15!!).  
-  (and (string-match "XEmacs" emacs-version) 'strict)
-  "*Whether Proof General is strict about the read-only region in buffers.
-If non-nil, an error is given when an attempt is made to edit the
-read-only region.  If nil, Proof General is more relaxed (but may give
-you a reprimand!).
+(defcustom proof-auto-delete-windows nil
+  "*If non-nil, automatically remove windows when they are cleaned.
+For example, at the end of a proof the goals buffer window will
+be cleared; if this flag is set it will automatically be removed.
+If you want to fix the sizes of your windows you may want to set this
+variable to 'nil' to avoid windows being deleted automatically.
+If you use multiple frames, only the windows in the currently
+selected frame will be automatically deleted."
+  :type 'boolean
+  :group 'proof-user-options)
 
-If you change proof-strict-read-only during a session, you must use
-\"Restart\" (proof-shell-restart)
+(defcustom proof-toolbar-use-button-enablers t
+  "*If non-nil, toolbars buttons may be enabled/disabled automatically.
+Toolbar buttons can be automatically enabled/disabled according to
+the context.  Set this variable to nil if you don't like this feature
+or if you find it unreliable.
 
-The default value for proof-strict-read-only depends on which
-version of Emacs you are using.  In FSF Emacs, strict read only is buggy
-when it used in conjunction with font-lock, so it is disabled by default."
+Notes: 
+* Toolbar enablers are only available with XEmacs 21 and later.
+* With this variable nil, buttons do nothing when they would
+otherwise be disabled.
+* If you change this variable it will only be noticed when you 
+next start Proof General."
   :type 'boolean
   :group 'proof-user-options)
 
@@ -196,8 +220,71 @@ files which are out of date with respect to the lodead buffers!"
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-auto-action-when-deactivating-scripting
-  nil
+(defcustom proof-script-indent nil
+  ;; Particular proof assistants can enable this if they feel
+  ;; confident about it.  (I don't). -da
+  "*If non-nil, enable indentation code for proof scripts.
+Currently the indentation code can be rather slow for large scripts,
+and is critical on the setting of regular expressions for particular
+provers.  Enable it if it works for you."  
+  :type 'boolean 
+  :group 'proof-user-options)
+
+(defcustom proof-prog-name-ask nil
+  "*If non-nil, query user which program to run for the inferior process."
+  :type 'boolean
+  :group 'proof-user-options)
+
+(defcustom proof-prog-name-guess nil
+  "*If non-nil, use `proof-guess-command-line' to guess proof-prog-name.
+This option is compatible with proof-prog-name-ask.
+No effect if proof-guess-command-line is nil."
+  :type 'boolean
+  :group 'proof-user-options)
+
+;; FIXME: rationalize and combine next two
+(defcustom proof-one-command-per-line nil
+  "*If non-nil, format for newlines after each proof command in a script.
+This option is not fully-functional at the moment."
+  :type 'boolean
+  :group 'proof-user-options)
+
+(defcustom proof-tidy-response
+  t
+  "*Non-nil indicates that the response buffer should be cleared often.
+The response buffer can be set either to accumulate output, or to
+clear frequently.  
+
+With this variable non-nil, the response buffer is kept tidy by
+clearing it often, typically between successive commands (just like the
+goals buffer).  
+
+Otherwise the response buffer will accumulate output from the prover."
+  :type 'boolean
+  :group 'proof-user-options)
+
+(defcustom proof-show-debug-messages t
+  "*Whether to display debugging messages in the response buffer.
+If non-nil, debugging messages are displayed in the response giving
+information about what Proof General is doing.
+To avoid erasing the messages shortly after they're printed, 
+you should set `proof-tidy-response' to nil."
+  :type 'boolean
+  :group 'proof-user-options)
+
+(defcustom proof-toolbar-follow-mode 'locked
+  "*Choice of how point moves with toolbar commands.
+One of the symbols: 'locked, 'follow, 'ignore.
+If 'locked, point sticks to the end of the locked region with toolbar commands.
+If 'follow, point moves just when needed to display the locked region end.
+If 'ignore, point is never moved after toolbar movement commands."
+  :type '(choice
+	  (const :tag "Follow locked region" locked)
+	  (const :tag "Keep locked region displayed" follow)
+	  (const :tag "Never move" ignore))
+  :group 'proof-user-options)
+
+(defcustom proof-auto-action-when-deactivating-scripting nil
   "*If 'retract or 'process, do that when deactivating scripting.
 
 With this option set to 'retract or 'process, when scripting 
@@ -220,23 +307,6 @@ is no locked region."
 	  (const :tag "Automatically process" process))
   :group 'proof-user-options)
 
-(defcustom proof-script-indent nil
-  ;; Particular proof assistants can enable this if they feel
-  ;; confident about it.  (I don't). -da
-  "*If non-nil, enable indentation code for proof scripts.
-Currently the indentation code can be rather slow for large scripts,
-and is critical on the setting of regular expressions for particular
-provers.  Enable it if it works for you."  
-  :type 'boolean 
-  :group 'proof-user-options)
-
-;; FIXME: rationalize and combine next two
-(defcustom proof-one-command-per-line nil
-  "*If non-nil, format for newlines after each proof command in a script.
-This option is not fully-functional at the moment."
-  :type 'boolean
-  :group 'proof-user-options)
-
 (defcustom proof-script-command-separator " "
   "*String separating commands in proof scripts.
 For example, if a proof assistant prefers one command per line, then 
@@ -259,45 +329,7 @@ The protocol used should be configured so that no user interaction
   :type 'string
   :group 'proof-user-options)
 
-(defcustom proof-auto-delete-windows nil
-  "*If non-nil, automatically remove windows when they are cleaned.
-For example, at the end of a proof the goals buffer window will
-be cleared; if this flag is set it will automatically be removed.
-If you want to fix the sizes of your windows you may want to set this
-variable to 'nil' to avoid windows being deleted automatically.
-If you use multiple frames, only the windows in the currently
-selected frame will be automatically deleted."
-  :type 'boolean
-  :group 'proof-user-options)
 
-(defcustom proof-splash-inhibit
-  nil
-  "*Non-nil prevents splash screen display when Proof General is loaded."
-  :type 'boolean
-  :group 'proof-user-options)
-
-(defcustom proof-tidy-response
-  t
-  "*Non-nil indicates that the response buffer should be cleared often.
-The response buffer can be set either to accumulate output, or to
-clear frequently.  
-
-With this variable non-nil, the response buffer is kept tidy by
-clearing it often, typically between successive commands (just like the
-goals buffer).  
-
-Otherwise the response buffer will accumulate output from the prover."
-  :type 'boolean
-  :group 'proof-user-options)
-
-(defcustom proof-show-debug-messages t
-  "*Whether to display debugging messages in the response buffer.
-If non-nil, debugging messages are displayed in the response giving
-information about what Proof General is doing.
-To avoid erasing the messages shortly after they're printed, 
-you should set `proof-tidy-response' to nil."
-  :type 'boolean
-  :group 'proof-user-options)
 
 
 
@@ -1432,17 +1464,9 @@ These are evaluated and appended to `proof-splash-contents'."
 
 
 ;;
-;; 8. x-symbol support
+;; 8. x-symbol configuration
 ;;
 
-(defcustom proof-x-symbol-support nil
-  "*Whether to use x-symbol in Proof General buffers.
-If you activate this variable, whether or not you get x-symbol support
-depends on if your proof assistant supports it and it is enabled
-inside your Emacs."
-  :type 'boolean
-  :group 'proof-user-options)
-
 (defgroup proof-x-symbol nil
   "Configuration of x-symbol for Proof General."
   :group 'proof
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e0471d5d..50797dfe 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1276,7 +1276,7 @@ the comment."
 
 
 ; Assert until point - We actually use this to implement the 
-; assert-until-point, active terminator keypress, and find-next-terminator. 
+; assert-until-point, electric terminator keypress, and find-next-terminator. 
 ; In different cases we want different things, but usually the information
 ; (i.e. are we inside a comment) isn't available until we've actually run
 ; proof-segment-up-to (point), hence all the different options when we've
@@ -1974,9 +1974,6 @@ No action if BUF is nil."
      ["Start proof assistant"
       proof-shell-start
       :active (not (proof-shell-live-buffer))]
-     ["Toggle scripting"
-      proof-toggle-active-scripting
-      :active t]
 ;     ["Restart scripting"
 ;      proof-shell-restart
 ;      :active (proof-shell-live-buffer)]
@@ -2006,18 +2003,23 @@ No action if BUF is nil."
 
 
 (defvar proof-menu  
-  (append '(["Active terminator" proof-active-terminator-minor-mode
+  (append '("----"
+	    ["Scripting active" proof-toggle-active-scripting
 	     :active t
 	     :style toggle
-             :selected proof-active-terminator-minor-mode]
+	     :selected (eq proof-script-buffer (current-buffer))]
+	    ["Electric terminator" proof-electric-terminator-toggle
+	     :active t
+	     :style toggle
+             :selected proof-electric-terminator-enable]
 	    ["Toolbar" proof-toolbar-toggle
 	     :active (featurep 'toolbar)
 	     :style toggle
-	     :selected (not proof-toolbar-inhibit)]
+	     :selected proof-toolbar-enable]
 	    ["X symbol" proof-x-symbol-toggle
 	     :active (proof-x-symbol-support-maybe-available)
 	     :style toggle
-	     :selected proof-x-symbol-support-on]
+	     :selected proof-x-symbol-enable]
 	    "----")
 	  ;; UGLY COMPATIBILITY  FIXME: remove this soon
           (list (if (string-match "XEmacs 19.1[2-9]" emacs-version)
@@ -2029,39 +2031,30 @@ No action if BUF is nil."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;          Active terminator minor mode                            ;;
+;;          Electric terminator minor mode                          ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; FIXME: Paul Callaghan wants to make the default for this be
-;; 't'.  Perhaps we need a user option which configures the default.
-;; Moreover, this minor mode is only relevant to scripting
-;; buffers, so a buffer-local setting may be inappropriate.
-(deflocal proof-active-terminator-minor-mode nil 
-  "Active terminator minor mode flag")
+;; Make sure proof-electric-terminator-enable is registered as
+;; a minor mode.
 
-;; Make sure proof-active-terminator-minor-mode is registered
-(or (assq 'proof-active-terminator-minor-mode minor-mode-alist)
+(or (assq 'proof-electric-terminator-enable minor-mode-alist)
     (setq minor-mode-alist
 	  (append minor-mode-alist
-		  (list '(proof-active-terminator-minor-mode
+		  (list '(proof-electric-terminator-enable
 			  (concat " " proof-terminal-string))))))
 
-(defun proof-active-terminator-minor-mode (&optional arg)
-  "Toggle Proof General's active terminator minor mode.
-With ARG, turn on the Active Terminator minor mode if and only if ARG
-is positive.
-
-If active terminator mode is enabled, pressing a terminator will 
-automatically activate `proof-assert-next-command' for convenience."
- (interactive "P")
- (setq proof-active-terminator-minor-mode
-       (if (null arg) (not proof-active-terminator-minor-mode)
-	 (> (prefix-numeric-value arg) 0)))
- (if (fboundp 'redraw-modeline)
-     (redraw-modeline)
-   (force-mode-line-update)))
-
-(defun proof-process-active-terminator ()
+;; This is a value used by custom-set property = proof-set-bool.
+(defun proof-electric-terminator-enable ()
+  "Make sure the modeline is updated to display new value for electric terminator."
+  ;; FIMXE: UGLY COMPATIBILITY HACK 
+  (if (fboundp 'redraw-modeline)
+      (redraw-modeline)
+    (force-mode-line-update)))
+
+(fset 'proof-electric-terminator-toggle 
+      (proof-customize-toggle proof-electric-terminator-enable))
+
+(defun proof-process-electric-terminator ()
   "Insert the proof command terminator, and assert up to it."
   (let ((mrk (point)) ins incomment)
     (if (looking-at "\\s-\\|\\'\\|\\w") 
@@ -2078,13 +2071,13 @@ automatically activate `proof-assert-next-command' for convenience."
     (or incomment
 	(proof-script-next-command-advance))))
 
-(defun proof-active-terminator ()
+(defun proof-electric-terminator ()
   "Insert the terminator, perhaps sending the command to the assistant.
-If proof-active-terminator-minor-mode is non-nil, the command will be
+If proof-electric-terminator-enable is non-nil, the command will be
 sent to the assistant."
   (interactive)
-  (if proof-active-terminator-minor-mode 
-      (proof-process-active-terminator)
+  (if proof-electric-terminator-enable 
+      (proof-process-electric-terminator)
     (self-insert-command 1)))
 
 
@@ -2221,14 +2214,14 @@ finish setup which depends on specific proof assistant configuration."
 
   ;; Additional key definitions which depend on configuration for
   ;; specific proof assistant.
-  ;; This is rather fragile: we assume terminal char is something
-  ;; sensible (and exists) for this to be set.
+  ;; FIXME da: robustify here.  
+  ;;   This is rather fragile: we assume terminal char is something
+  ;;   sensible (and exists) for this to be set.
   (define-key proof-mode-map
     (vconcat [(control c)] (vector proof-terminal-char))
-    'proof-active-terminator-minor-mode)
-
+    'proof-electric-terminator-toggle)
   (define-key proof-mode-map (vector proof-terminal-char)
-    'proof-active-terminator)
+    'proof-electric-terminator)
 
   (make-local-variable 'indent-line-function)
   (if proof-script-indent
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index f3d48107..e6a0e523 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -84,10 +84,11 @@ Borrowed from startup-center-spaces."
   "Save window config and display Proof General splash screen.
 Only do it if proof-splash-display is nil."
   (if (and
+       proof-splash-enable
+       ;; FIXME: UGLY COMPATIBILITY HACK
        ;; Next check avoids XEmacs giving "Arithmetic Error"
        ;; during byte compilation.
-       (if (fboundp 'noninteractive) (not (noninteractive)) t)
-       (not proof-splash-inhibit))
+       (if (fboundp 'noninteractive) (not (noninteractive)) t))
     (let
 	;; Keep win config explicitly instead of pushing/popping because
 	;; if the user switches windows by hand in some way, we want
@@ -157,7 +158,7 @@ Only do it if proof-splash-display is nil."
       (setq unread-command-event (next-command-event)))
   (remove-hook 'proof-mode-hook 'proof-splash-timeout-waiter))
 
-(unless proof-splash-inhibit
+(if proof-splash-enable
   (add-hook 'proof-mode-hook 'proof-splash-timeout-waiter))
 
 (provide 'proof-splash)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 963f3da8..586d0ffb 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -128,7 +128,7 @@ and chooses the best one for the display properites.")
        (menuname      (cadr tle))
        (tooltip       (nth 2 tle))
        (existsenabler (nth 3 tle))
-       (enablep	      (and proof-toolbar-use-enablers
+       (enablep	      (and proof-toolbar-use-button-enablers
 			   (>= emacs-major-version 21)
 			   existsenabler))
        (enabler	      (proof-toolbar-enabler token))
@@ -170,7 +170,7 @@ to the default toolbar."
   (interactive)
   (if (featurep 'toolbar)		; won't work in FSF Emacs
       (if (and	
-	   (not proof-toolbar-inhibit)
+	   proof-toolbar-enable
 	   ;; NB for FSFmacs use window-system, not console-type
 	   (eq (console-type) 'x))
 	  (let
@@ -215,12 +215,10 @@ to the default toolbar."
 	(if proof-toolbar-itimer (delete-itimer proof-toolbar-itimer))
 	(setq proof-toolbar-itimer nil))))
 
-(defun proof-toolbar-toggle (&optional force-on)
-  "Toggle display of Proof General toolbar.  With optional ARG, force on."
-  (interactive "P")
-  (setq proof-toolbar-inhibit
-       (or force-on (not proof-toolbar-inhibit)))
-  (proof-toolbar-setup))
+;; Action to take after altering proof-toolbar-enable
+(defalias 'proof-toolbar-enable 'proof-toolbar-setup)
+(fset 'proof-toolbar-toggle 
+      (proof-customize-toggle proof-toolbar-enable))
 
 (deflocal proof-toolbar-refresh-flag nil
   "Flag indicating that the toolbar should be refreshed.")
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index cd482247..c08ff8d9 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -12,11 +12,6 @@
 ;; proof-x-symbol.el,v 2.4 1999/08/23 18:38:40 da Exp
 ;;
 
-;; Idea is that Proof General will only let this next variable
-;; become t if all the necessary infrastructure is in place.
-(defvar proof-x-symbol-support-on nil
-  "Non-nil if x-symbol support is currently switched on.")
-
 (defvar proof-x-symbol-initialized nil
   "Non-nil if x-symbol support has been initialized.")
 
@@ -28,16 +23,6 @@
 	   (require 'x-symbol-autoloads) 
 	 (t (featurep 'x-symbol-autoloads)))))
 
-;;;###autoload
-(defun proof-x-symbol-toggle (&optional force-on)
-  "Toggle support for x-symbol.  With optional ARG, force on."
-  (interactive "P")
-  (let ((enable  (or force-on (not proof-x-symbol-support-on))))
-    ;; Initialize if it hasn't been done already
-    (if (and enable (not proof-x-symbol-initialized))
-	(proof-x-symbol-initialize 'giveerrors))
-    (setq proof-x-symbol-support-on enable)
-    (proof-x-symbol-mode-all-buffers)))
 
 (defun proof-x-symbol-initialize (&optional error)
   "Initialize x-symbol support for Proof General, if possible.
@@ -126,10 +111,21 @@ If ERROR is non-nil, give error on failure, otherwise a warning."
 	;; Finished.
 	(setq proof-x-symbol-initialized t))))))
 
+;;;###autoload
+(defun proof-x-symbol-enable ()
+  "Turn on or off support for x-symbol, initializing if necessary."
+  (if (and proof-x-symbol-enable (not proof-x-symbol-initialized))
+      (proof-x-symbol-initialize 'giveerrors))
+  (proof-x-symbol-mode-all-buffers))
+
+;; A toggling function for the menu.
+;;;###autload
+(fset 'proof-x-symbol-toggle
+      (proof-customize-toggle proof-x-symbol-enable))
 
 (defun proof-x-symbol-decode-region (start end) 
   "Call (x-symbol-decode-region START END), if x-symbol support is enabled."
-  (if proof-x-symbol-support-on
+  (if proof-x-symbol-enable
       (x-symbol-decode-region start end)))
 
 (defun proof-x-symbol-encode-shell-input ()
@@ -151,13 +147,13 @@ A value for proof-shell-insert-hook."
 
 ;; ### autoload
 (defun proof-x-symbol-mode ()
-  "Turn on/off x-symbol mode in current buffer, from proof-x-symbol-support-on."
+  "Turn on/off x-symbol mode in current buffer, from proof-x-symbol-enable."
   (interactive)
   (if proof-x-symbol-initialized
       (progn
 	(setq x-symbol-language proof-assistant-symbol)
 	(if (eq x-symbol-mode 
-		(not proof-x-symbol-support-on))
+		(not proof-x-symbol-enable))
 	    (x-symbol-mode)) ;; DvO: this is a toggle
 	;; Needed ?  Should let users do this in the 
 	;; usual way, if it works.
@@ -173,7 +169,7 @@ A value for proof-shell-insert-hook."
 
 (defun proof-x-symbol-mode-all-buffers ()
   "Activate/deactivate x-symbol mode in all Proof General buffers.
-A subroutine of proof-x-symbol-toggle"
+A subroutine of proof-x-symbol-enable."
   (proof-with-current-buffer-if-exists 
    proof-shell-buffer
    (proof-x-symbol-shell-config))
@@ -194,7 +190,7 @@ Assumes that the current buffer is the proof shell buffer."
   (if proof-x-symbol-initialized
       (progn
 	(cond
-	 (proof-x-symbol-support-on
+	 (proof-x-symbol-enable
 	  (if (and proof-xsym-activate-command 
 		   (proof-shell-live-buffer))
 	      (proof-shell-invisible-command 
@@ -202,7 +198,7 @@ Assumes that the current buffer is the proof shell buffer."
 	  ;; Do the encoding as the first step of input manipulation
 	  (add-hook 'proof-shell-insert-hook
 		    'proof-x-symbol-encode-shell-input))
-	 ((not proof-x-symbol-support-on)
+	 ((not proof-x-symbol-enable)
 	  (if (and proof-xsym-deactivate-command 
 		   (proof-shell-live-buffer))
 	      (proof-shell-invisible-command 
@@ -217,11 +213,14 @@ Assumes that the current buffer is the proof shell buffer."
 
 
 ;;
-;; Initialize x-symbol-support on load-up if user has asked for it
+;; Try to initialize x-symbol-support on load-up if user has asked for it
 ;;
+(if proof-x-symbol-enable (proof-x-symbol-initialize))
 ;;
-(if proof-x-symbol-support (proof-x-symbol-initialize))
-
+;; If initialization failed, the next line will turn off
+;; proof-x-symbol-enable for the session.
+;;
+(customize-set-variable 'proof-x-symbol-enable proof-x-symbol-initialized)
 
 
 
diff --git a/generic/proof.el b/generic/proof.el
index df94cb91..90813468 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -21,8 +21,6 @@
 ;; cl is dumped with my XEmacs 20.4, but not FSF Emacs 20.2.
 (require 'cl)				
 
-
-
 (require 'proof-config)			; configuration variables
 
 (require 'proof-splash)			; display splash screen
@@ -148,6 +146,11 @@ read.")
 ;;; Utilities/macros used in several files  (-> proof-utils)
 ;;;
 
+;;
+;; 
+
+
+
 ;; -----------------------------------------------------------------
 ;; Handy macros
 
@@ -157,6 +160,18 @@ read.")
        (with-current-buffer ,buf
 	 ,@body)))
 
+(defmacro proof-customize-toggle (var)
+  "Make a function for toggling a boolean customize setting VAR."
+  `(lambda (arg)
+     ,(concat "Toggle " (symbol-name var) ". With ARG, turn on iff ARG>0.
+This function simply uses customize-set-variable to set the variable.
+It was constructed with the macro proof-customize-toggle.")
+     (interactive "P")
+     (customize-set-variable 
+      (quote ,var)
+      (if (null arg) (not ,var)
+	(> (prefix-numeric-value arg) 0)))))
+
 ;; -----------------------------------------------------------------
 ;; Buffers and filenames