From dacba6c398ece6ea00677ce77c7377dcf82aae23 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 26 May 2000 18:05:08 +0000
Subject: Switch to using per-prover generic option for x-symbol-enable.

---
 generic/proof-x-symbol.el | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index cf084146..52a9d6e8 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -137,11 +137,11 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
 (defun proof-x-symbol-enable ()
   "Turn on or off support for x-symbol, initializing if necessary.
 Calls proof-x-symbol-toggle-clean-buffers afterwards."
-  (if (and proof-x-symbol-enable (not proof-x-symbol-initialized))
+  (if (and (proof-ass x-symbol-enable) (not proof-x-symbol-initialized))
       (progn
-	(setq proof-x-symbol-enable nil) ; assume failure!
+	(set (proof-ass-sym x-symbol-enable) nil) ; assume failure!
 	(proof-x-symbol-initialize 'giveerrors)
-	(setq proof-x-symbol-enable t)))
+	(set (proof-ass-sym x-symbol-enable) t)))
   (proof-x-symbol-mode-all-buffers)
   (proof-x-symbol-toggle-clean-buffers))
 
@@ -152,7 +152,7 @@ Calls proof-x-symbol-toggle-clean-buffers afterwards."
   "Clear the response buffer and send proof-showproof-command.
 This function is intended to clean the display after a change
 in the status of X-Symbol display.
-This is a subroutine of x-symbol-enable."
+This is a subroutine of proof-x-symbol-enable."
   (proof-shell-maybe-erase-response nil t t)
   (if (and proof-showproof-command (proof-shell-available-p))
     (proof-shell-invisible-command proof-showproof-command)))
@@ -161,7 +161,7 @@ This is a subroutine of x-symbol-enable."
 (defun proof-x-symbol-decode-region (start end) 
   "Call (x-symbol-decode-region A Z), if x-symbol support is enabled.
 This converts tokens in the region into X-Symbol characters."
-  (if (and proof-x-symbol-enable)
+  (if (and (proof-ass x-symbol-enable))
       (x-symbol-decode-region start end)))
 
 (defun proof-x-symbol-encode-shell-input ()
@@ -227,7 +227,7 @@ takes place (it isn't used for output-only buffers)."
 	  ;; Buffers which have XS minor mode toggled always keep 
 	  ;; x-symbol-language set.
 	  (setq x-symbol-language proof-assistant-symbol)
-	  (x-symbol-mode (if proof-x-symbol-enable 1 0))
+	  (x-symbol-mode (if (proof-ass x-symbol-enable) 1 0))
 	  ;; Font lock mode must be engaged for x-symbol to do its job
           ;; properly, at least when there is no mule around.
 	  (if (and x-symbol-mode (not (featurep 'mule)))
@@ -254,7 +254,7 @@ Assumes that the current buffer is the proof shell buffer."
   (if proof-x-symbol-initialized
       (progn
 	(cond
-	 (proof-x-symbol-enable
+	 ((proof-ass x-symbol-enable)
 	  (setq x-symbol-language proof-assistant-symbol)
 	  (if (and proof-xsym-activate-command 
 		   (proof-shell-live-buffer))
@@ -263,7 +263,7 @@ Assumes that the current buffer is the proof shell buffer."
 	  ;; We do encoding as the first step of input manipulation
 	  (add-hook 'proof-shell-insert-hook
 		    'proof-x-symbol-encode-shell-input))
-	 ((not proof-x-symbol-enable)
+	 ((not (proof-ass x-symbol-enable))
 	  (if (and proof-xsym-deactivate-command 
 		   (proof-shell-live-buffer))
 	      (proof-shell-invisible-command 
@@ -279,7 +279,7 @@ Assumes that the current buffer is the proof shell buffer."
 ;;;###autoload
 (defun proof-x-symbol-configure ()
   "Configure the current buffer (goals or response) for X-Symbol."
-  (if proof-x-symbol-enable
+  (if (proof-ass x-symbol-enable)
       (progn
 	(setq x-symbol-language proof-assistant-symbol)
 	;; If we're turning on x-symbol, attempt to convert to 
@@ -299,14 +299,13 @@ Assumes that the current buffer is the proof shell buffer."
 ;;
 ;; 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 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)
-
-
+(if (proof-ass x-symbol-enable) 
+    (progn
+      (proof-x-symbol-initialize)
+      (unless proof-x-symbol-initialized
+	;; If initialization failed, turn off
+	;; x-symbol-enable for the session.
+	(customize-set-variable (proof-ass-sym x-symbol-enable) nil))))
 
 (provide 'proof-x-symbol)
 ;; End of proof-x-symbol.el
-- 
cgit v1.2.3