Generic support for x-symbol tuned up.

5 files changed, 100 insertions, 90 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 781a3b56..f2320327 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2022,9 +2022,13 @@ No action if BUF is nil."
 	     :style toggle
              :selected proof-active-terminator-minor-mode]
 	    ["Toolbar" proof-toolbar-toggle
-	       :active (featurep 'toolbar)
-	       :style toggle
-	       :selected (not proof-toolbar-inhibit)]
+	     :active (featurep 'toolbar)
+	     :style toggle
+	     :selected (not proof-toolbar-inhibit)]
+	    ["X symbol" proof-x-symbol-toggle
+	     :active (proof-x-symbol-support-maybe-available)
+	     :style toggle
+	     :selected proof-x-symbol-support-on]
 	    "----")
 	  ;; UGLY COMPATIBILITY  FIXME: remove this soon
           (list (if (string-match "XEmacs 19.1[2-9]" emacs-version)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index ccd117e2..3c80c790 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -292,13 +292,6 @@ Does nothing if proof assistant is already running."
 	    proof-response-buffer (get-buffer-create 
 				     (concat "*" proc "-response*")))
 
-      ;; FIXME: this function should be invoked elsewhere: 
-      ;; probably via hook functions.
-;       (proof-x-symbol-toggle (if proof-x-symbol-support 1 0))     ;; DvO
-;       (and (featurep 'x-symbol)
-; 	   (proof-x-symbol-mode-all-buffers proof-x-symbol-support-on)) ;; DvO
-      (proof-x-symbol-mode-all-buffers)
-
       (save-excursion
 	(set-buffer proof-shell-buffer)
 	
@@ -1708,7 +1701,9 @@ before and after sending the command."
     (set-buffer proof-goals-buffer)
     (proof-font-lock-minor-mode)
     ;; Turn off the display of annotations here
-    (proof-shell-dont-show-annotations)))
+    (proof-shell-dont-show-annotations)
+    ;; Maybe turn on x-symbols
+    (proof-x-symbol-mode)))
 
 (defun proof-response-config-done ()
   "Initialise the response buffer after the child has been configured."
@@ -1716,11 +1711,15 @@ before and after sending the command."
     (set-buffer proof-response-buffer)
     (proof-font-lock-minor-mode)
     ;; Turn off the display of annotations here
-    (proof-shell-dont-show-annotations)))
+    (proof-shell-dont-show-annotations)
+    ;; Maybe turn on x-symbols
+    (proof-x-symbol-mode)))
 
 
 (defun proof-shell-config-done ()
-  "Initialise the specific prover after the child has been configured."
+  "Initialise the specific prover after the child has been configured.
+Every derived shell mode should call this function at the end of
+processing."
   (save-excursion			
     (set-buffer proof-shell-buffer)
     (let ((proc (get-buffer-process proof-shell-buffer)))
@@ -1738,7 +1737,10 @@ before and after sending the command."
       ;; initialised. 
       (if proof-shell-init-cmd
 	  (proof-shell-invisible-command proof-shell-init-cmd t)
-	(setq proof-action-list nil)))))
+	(setq proof-action-list nil))
+      
+      ;; Configure for x-symbol
+      (proof-x-symbol-shell-config))))
 
 (eval-and-compile
 (define-derived-mode proof-universal-keys-only-mode fundamental-mode
@@ -1762,7 +1764,6 @@ before and after sending the command."
   (setq proof-buffer-type 'response)
   (easy-menu-add proof-response-mode-menu proof-response-mode-map)))
 
-
 (easy-menu-define proof-response-mode-menu
 		  proof-response-mode-map
 		  "Menu for Proof General response buffer."
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index e154e73e..963f3da8 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -216,7 +216,7 @@ to the default toolbar."
 	(setq proof-toolbar-itimer nil))))
 
 (defun proof-toolbar-toggle (&optional force-on)
-  "Toggle display of Proof General toolbar."
+  "Toggle display of Proof General toolbar.  With optional ARG, force on."
   (interactive "P")
   (setq proof-toolbar-inhibit
        (or force-on (not proof-toolbar-inhibit)))
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index a4053ebb..9dad0d4c 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -20,36 +20,29 @@
 (defvar proof-x-symbol-initialized nil
   "Non-nil if x-symbol support has been initialized.")
 
+;;; ###autoload
+(defun proof-x-symbol-support-maybe-available ()
+  "A test to see whether x-symbol support may be available."
+  (and (eq (console-type) 'x)
+       (condition-case ()
+	   (require 'x-symbol-autoloads) 
+	 (t (featurep 'x-symbol-autoloads)))))
+
 ;;;###autoload
-(defun proof-x-symbol-toggle (&optional arg)
-  "Toggle support for x-symbol.  With optional ARG, force on if ARG<>0.
-In other words, you can type M-1 M-x proof-x-symbol-toggle to turn it
-on, M-0 M-x proof-x-symbol-toggle to turn it off."
-  (interactive "p")
-  (let ((enable  (or (and arg (> arg 0))
-		     (if arg;;DvO to DA: why that difficult calculations?
-			 ;; da: see explanation I've put in docstring.
-			 ;; probably over the top!
-			 (and (not (= arg 0))
-			      (not proof-x-symbol-support-on))
-		       (not proof-x-symbol-support-on)))))
+(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 (eq proof-x-symbol-support-on 'init) enable)
+    (if (and enable (not proof-x-symbol-initialized))
 	(proof-x-symbol-initialize 'giveerrors))
-    ;; Turn on or off support in prover
-    ;; FIXME: need to decide how best to do this?
-    ;; maybe by editing proof-init-cmd, but also want to turn
-    ;; x-symbol on/off during use perhaps.
-    ;; Hacking init command is a bit ugly!
-    (if (and enable proof-xsym-activate-command)
-	(proof-shell-invisible-command proof-xsym-activate-command))
-    (if (and (not enable) proof-xsym-deactivate-command)
-	(proof-shell-invisible-command proof-xsym-activate-command))
-    (setq proof-x-symbol-support-on enable)))
+    (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.
 If ERROR is non-nil, give error on failure, otherwise a warning."
+  (interactive)
   (unless proof-x-symbol-initialized
     (let* 
 ;;; Values for x-symbol-register-language are constructed
@@ -156,67 +149,71 @@ A value for proof-shell-insert-hook."
                (prog1 (buffer-substring)
                  (kill-buffer (current-buffer)))))))
 
+;; ### autoload
 (defun proof-x-symbol-mode ()
-  "Hook function to turn on/off x-symbol mode in the current buffer."
-    (setq x-symbol-language proof-assistant-symbol)
-    (if (eq x-symbol-mode 
-	    (not proof-x-symbol-support-on))
-	(x-symbol-mode)) ;; DvO: this is a toggle
-    ;; Needed ?  Should let users do this in the 
-    ;; usual way, if it works.
-    (if (and x-symbol-mode 
-	     (not font-lock-mode));;DvO
-	(font-lock-mode)
-      (unless (featurep 'mule)
-	(x-symbol-nomule-fontify-cstrings))));;DvO
-
-;; FIXME: this is called in proof-shell-start, but perhaps
-;; it would be better enabled via hooks for the mode 
-;; functions?  Or somewhere else?  (Problem at the moment
-;; is that we don't get x-symbol in script buffers before
-;; proof assistant is started, presumably).
-;;
-;; Suggestion: add functions
-;;
-;;  proof-x-symbol-activate
-;;  proof-x-symbol-deactivate
-;;
-;; which do what this function does, but also add/remove
-;; hooks for shell mode, etc, 'proof-x-symbol-mode. 
-;; (or variation of that function to just turn x-symbol mode
-;;  *on*).
+  "Turn on or off x-symbol mode in the current buffer."
+  (if proof-x-symbol-initialized
+      (progn
+	(setq x-symbol-language proof-assistant-symbol)
+	(if (eq x-symbol-mode 
+		(not proof-x-symbol-support-on))
+	    (x-symbol-mode)) ;; DvO: this is a toggle
+	;; Needed ?  Should let users do this in the 
+	;; usual way, if it works.
+	(if (and x-symbol-mode 
+		 (not font-lock-mode));;DvO
+	    (font-lock-mode)
+	  ;; da: Is this supposed to be called only if we don't turn on
+	  ;; font-lock???
+	  (unless (featurep 'mule)
+	    (if (fboundp 'x-symbol-nomule-fontify-cstrings)
+		(x-symbol-nomule-fontify-cstrings)))))));;DvO
+
 
-;; ### autoload
 (defun proof-x-symbol-mode-all-buffers ()
-  "Activate/deactivate x-symbol in Proof General shell, goals, and response buffer."
+  "Activate/deactivate x-symbol mode in all Proof General buffers.
+A subroutine of proof-x-symbol-toggle"
+  (proof-with-current-buffer-if-exists 
+   proof-shell-buffer
+   (proof-x-symbol-shell-config))
+  (let
+      ((bufs   (append
+		(list proof-goals-buffer proof-response-buffer)
+		(proof-buffers-in-mode proof-mode-for-script))))
+    (while bufs
+      ;; mapcar doesn't work with macros
+      (proof-with-current-buffer-if-exists (car bufs)
+					   (proof-x-symbol-mode))
+      (setq bufs (cdr bufs)))))
+
+;; #### autoload
+(defun proof-x-symbol-shell-config ()
+  "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil."
   (if proof-x-symbol-initialized
-      (progn
-	(if proof-x-symbol-support-on
-	    (add-hook 'proof-shell-insert-hook
-		      'proof-x-symbol-encode-shell-input)
-	  (remove-hook 'proof-shell-insert-hook
-		       'proof-x-symbol-encode-shell-input)
-	  (remove-hook 'comint-output-filter-functions
-		       'x-symbol-comint-output-filter))
-	(save-excursion
-	  (and proof-shell-buffer
-	       (set-buffer proof-shell-buffer)
-	       (proof-x-symbol-mode))
-	  (and proof-goals-buffer
-	       (set-buffer proof-goals-buffer)
-	       (proof-x-symbol-mode))
-	  (and proof-response-buffer
-	       (set-buffer proof-response-buffer)
-	       (proof-x-symbol-mode))))))
+      (cond
+       (proof-x-symbol-support-on
+	(if (and proof-xsym-activate-command (proof-shell-live-buffer))
+	    (proof-shell-invisible-command proof-xsym-activate-command 'wait))
+	(add-hook 'proof-shell-insert-hook
+		  'proof-x-symbol-encode-shell-input))
+       ((not proof-x-symbol-support-on)
+	(if (and proof-xsym-deactivate-command (proof-shell-live-buffer))
+	    (proof-shell-invisible-command proof-xsym-deactivate-command 'wait))
+	(remove-hook 'proof-shell-insert-hook
+		     'proof-x-symbol-encode-shell-input)
+	(remove-hook 'comint-output-filter-functions
+		     'x-symbol-comint-output-filter)))
+    ;; switch the mode on/off in the buffer
+    (proof-x-symbol-mode)))
+
 
 
 ;;
 ;; Initialize x-symbol-support on load-up if user has asked for it
 ;;
+;;
 (if proof-x-symbol-support (proof-x-symbol-initialize))
 
-;; Need a hook in shell to do this, maybe
-;; (if proof-x-symbol-initialized (proof-x-symbol-toggle 1))
 
 
 
diff --git a/generic/proof.el b/generic/proof.el
index 2f43540f..f768e731 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -78,9 +78,11 @@
 (autoload 'proof-x-symbol-decode-region "proof-x-symbol"
   "Call (x-symbol-decode-region START END), if x-symbol support is enabled.")
 
-(autoload 'proof-x-symbol-mode-all-buffers "proof-x-symbol"
+(autoload 'proof-x-symbol-shell-config "proof-x-symbol"
   "Activate/deactivate x-symbol in Proof General shell, goals, and response buffer.")
 
+(autoload 'proof-x-symbol-mode "proof-x-symbol"
+  "Turn on or off x-symbol mode in the current buffer.")
 
 ;;;
 ;;; Global variables
@@ -156,6 +158,12 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
          (define-key map k f)))
    kbl))
 
+(defmacro proof-with-current-buffer-if-exists (buf &rest body)
+  "As with-current-buffer if BUF exists, otherwise nothing."
+  `(if (buffer-live-p ,buf)
+       (with-current-buffer ,buf
+	 ,@body)))
+
 ;; FIXME: this function should be combined with
 ;; proof-shell-maybe-erase-response-buffer.  Should allow
 ;; face of nil for unfontified output.