Extensive fixes for x-symbol and font-lock.

5 files changed, 145 insertions, 116 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index ea1e038e..7703c08e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,8 +1,7 @@
 ;; proof-config.el  Proof General configuration for proof assistant
 ;;
 ;; Copyright (C) 1998,9 LFCS Edinburgh. 
-;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
-;;          Thomas Kleymann and Dilip Sequeira
+;; Authors: David Aspinall
 ;;
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
@@ -29,7 +28,7 @@
 ;;     5c. hooks
 ;;  6. Goals buffer configuration
 ;;  7. Splash screen settings
-;;  8. x-symbol support
+;;  8. X-Symbol support
 ;;  9. Global constants 
 ;;
 ;; The user options don't need to be set on a per-prover basis,
@@ -1464,39 +1463,47 @@ These are evaluated and appended to `proof-splash-contents'."
 
 
 ;;
-;; 8. x-symbol configuration
+;; 8. X-Symbol configuration
 ;;
 
 (defgroup proof-x-symbol nil
-  "Configuration of x-symbol for Proof General."
+  "Configuration of X-Symbol for Proof General."
   :group 'proof
   :prefix "proof-xsym-")
 
-(defcustom proof-xsym-activate-command nil
-  "Command to activate symbol printing for x-symbols.
-If non-nil, this command is sent to the proof assistant when 
-x-symbol support is activated."
-  :type 'string
+(defcustom proof-xsym-extra-modes nil
+  "List of additional mode names to use X-Symbol with Proof General tokens.
+These modes will have X-Symbol enabled for the proof assistant token language,
+in addition to the four modes for Proof General (script, shell, response, pbp).
+
+Set this variable if you want additional modes to also display 
+tokens (for example, editing documentation or source code files)."
+  :type '(repeat symbol)
+  :group 'proof-x-symbol)
+
+(defcustom proof-xsym-extra-modes nil
+  "List of additional mode names to use X-Symbol with Proof General tokens.
+These modes will have X-Symbol enabled for the proof assistant token language,
+in addition to the four modes for Proof General (script, shell, response, pbp).
+
+Set this variable if you want additional modes to also display 
+tokens (for example, editing documentation or source code files)."
+  :type '(repeat symbol)
+  :group 'proof-x-symbol)
+
+(defcustom proof-xsym-font-lock-keywords nil
+  "Font lock keywords to use for the proof assistants X-Symbol token language."
+  :type 'sexp
   :group 'proof-x-symbol)
 
 (defcustom proof-xsym-deactivate-command nil
-  "Command to activate symbol printing for x-symbols.
+  "Command to deactivate token input/output for X-Symbol.
 If non-nil, this command is sent to the proof assistant when 
-x-symbol support is activated."
+X-Symbol support is deactivated."
   :type 'string
   :group 'proof-x-symbol)
 
 
-;; FIXME: add here the variables which have per-prover names at the
-;; moment.  Later we can autogenerate aliases for the prover-specific
-;; instances.  Will also need to rename, if possible.
-;; 
-;;  e.g.   x-symbol-isa-modes   becomes   isa-x-symbol-modes
-;;			       alias for  proof-x-symbol-modes
-;;
-
-  
-
 
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 76e2e510..5805d0e6 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2040,7 +2040,7 @@ No action if BUF is nil."
 	     :active (featurep 'toolbar)
 	     :style toggle
 	     :selected proof-toolbar-enable]
-	    ["X symbol" proof-x-symbol-toggle
+	    ["X-Symbol" proof-x-symbol-toggle
 	     :active (proof-x-symbol-support-maybe-available)
 	     :style toggle
 	     :selected proof-x-symbol-enable]
@@ -2280,12 +2280,22 @@ finish setup which depends on specific proof assistant configuration."
   ;; Put the ProofGeneral menu on the menubar
   (easy-menu-add proof-mode-menu proof-mode-map)
 
-  ;; For fontlock
-
-  ;; setting font-lock-defaults explicitly is required by FSF Emacs
-  ;; 20.2's version of font-lock
-  (make-local-variable 'font-lock-defaults)
-  (setq font-lock-defaults '(font-lock-keywords))
+  ;;
+  ;; Fontlock.
+  ;; 
+  ;; At the moment, the specific code hacks font-lock-keywords.
+  ;; Here we use the value there to hack font-lock-defaults, which
+  ;; is used by font-lock to set font-lock-keywords from again!!  
+  ;; Yuk.
+  ;; Previously, font-lock-keywords was used directly as a setting
+  ;; for the defaults.  This has a bad interaction with x-symbol
+  ;; which edits font-lock-keywords and loses the setting.  
+  ;; So we make a copy of it in a new variable.
+  ;; 
+  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
+  (make-local-variable 'proof-font-lock-defaults)
+  (setq proof-font-lock-defaults font-lock-keywords)
+  (setq font-lock-defaults '(proof-font-lock-defaults))
 
   ;; FIXME (da): zap commas support is too specific, should be enabled
   ;; by each proof assistant as it likes.
@@ -2299,6 +2309,7 @@ finish setup which depends on specific proof assistant configuration."
   (if (boundp 'font-lock-always-fontify-immediately)
       (progn
 	(make-local-variable 'font-lock-always-fontify-immediately)
+;; FIXME testing: this was "t".
 	(setq font-lock-always-fontify-immediately nil)))
 
   ;; Assume font-lock case folding follows proof-case-fold-search
@@ -2362,7 +2373,9 @@ finish setup which depends on specific proof assistant configuration."
   (or (buffer-file-name)
       (setq buffer-offer-save t))
 
-  ;; Maybe turn on x-symbol mode
+  ;; Maybe turn on x-symbol mode  
+  ;;  [no need for script mode files to be on xsymbol-auto-mode-alist;
+  ;;   having the switch here takes care of non-files]
   (proof-x-symbol-mode))
 
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 026ff435..f6a23800 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1676,10 +1676,6 @@ before and after sending the command."
   ;; (Problem to fix is that process can die before sentinel is set:
   ;;  it ought to be set just here, perhaps: but setting hook here
   ;;  had no effect for some odd reason).
-
-  ;; da added this 23/8/99.  LEGO sets font-lock-terms in shell,
-  ;; but didn't use it until now.
-  (proof-font-lock-minor-mode)
   ))
 
 ;; watch difference with proof-shell-menu, proof-shell-mode-menu.
@@ -1693,19 +1689,24 @@ before and after sending the command."
 
 
 
-(defun proof-font-lock-minor-mode ()
-  "Start font-lock as a minor mode in the current buffer."
+(defun proof-font-lock-configure-defaults ()
+  "Set defaults for font-lock based on current font-lock-keywords."
   ;; setting font-lock-defaults explicitly is required by FSF Emacs
   ;; 20.2's version of font-lock
-  (make-local-variable 'font-lock-defaults)
-  (setq font-lock-defaults '(font-lock-keywords))
-  (font-lock-set-defaults))
+  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
+  (make-local-variable 'proof-font-lock-defaults)
+  (setq proof-font-lock-defaults font-lock-keywords)
+  (setq font-lock-defaults '(proof-font-lock-defaults))
+  ;; Turn on fontification only if the user has configured it
+  ;; everywhere in general.
+  (if font-lock-auto-fontify
+      (turn-on-font-lock)))
 
 (defun proof-goals-config-done ()
   "Initialise the goals buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-goals-buffer)
-    (proof-font-lock-minor-mode)
+    (proof-font-lock-configure-defaults)
     ;; Turn off the display of annotations here
     (proof-shell-dont-show-annotations)
     ;; Maybe turn on x-symbols
@@ -1715,7 +1716,7 @@ before and after sending the command."
   "Initialise the response buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-response-buffer)
-    (proof-font-lock-minor-mode)
+    (proof-font-lock-configure-defaults)
     ;; Turn off the display of annotations here
     (proof-shell-dont-show-annotations)
     ;; Maybe turn on x-symbols
@@ -1728,6 +1729,9 @@ Every derived shell mode should call this function at the end of
 processing."
   (save-excursion			
     (set-buffer proof-shell-buffer)
+
+    (proof-font-lock-configure-defaults)
+
     (let ((proc (get-buffer-process proof-shell-buffer)))
       ;; Add the kill buffer function and process sentinel
       (make-local-hook 'kill-buffer-hook)
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 59fac3b9..697956e3 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -5,7 +5,7 @@
 ;;
 ;; With thanks to David von Oheimb for providing the original 
 ;; patches for using x-symbol with Isabelle Proof General, 
-;; and suggesting improvements here.
+;; and helping to write this file.
 ;;
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
@@ -28,44 +28,16 @@
   "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
-;;; from proof-assistant-symbol.
-;;; To initialise we call, for example:
-;;;
-;;;  (x-symbol-register-language 'isa x-symbol-isa x-symbol-isa-modes)
-;;;
-	((assistant	(symbol-name proof-assistant-symbol))
-	 (xs-lang	proof-assistant-symbol)
-	 (xs-feature	(intern (concat "x-symbol-" assistant)))
-	 (xs-modes	(intern (concat "x-symbol-" assistant "-modes")))
-	 (am-entry      (list xs-modes t xs-lang))
-	 (symmode-nm	(concat assistant "sym-mode"))
-	 (sym-flks	(intern (concat symmode-nm "-font-lock-keywords")))
-	 (symmode       (intern symmode-nm))
-	 ;;
-	 ;; Standard modes for using x-symbol. 
-	 ;;
-	 ;; NB: there is a problem with initialization order here,
-	 ;; these variables are set in script/shell mode initialization.
-	 ;; They ought to be set earlier, and enforced as part of the
-	 ;; generic scheme.   For the time being, these should appear 
-	 ;; on xs-modes (later that setting could be optional).
-;	 (stnd-modes	(list
-;			 proof-mode-for-script
-;			 proof-mode-for-shell
-;			 proof-mode-for-pbp
-;			 proof-mode-for-response))
-	 ;; 
-	 ;;
+  ; (unless proof-x-symbol-initialized
+    (let*
+	((assistant	 (symbol-name proof-assistant-symbol))
+	 (xs-feature     (concat "x-symbol-" assistant))
+	 (xs-feature-sym (intern xs-feature))
 	 ;; utility fn
 	 (error-or-warn	 
 	  (lambda (str) (if error (error str) (warn str)))))
-
-      ;;
-      ;; Now check that support is provided.
       ;;
+      ;; Check that support is provided.
       (cond
        ;;
        ;; First, some checks on x-symbol.
@@ -73,7 +45,7 @@ If ERROR is non-nil, give error on failure, otherwise a warning."
        ((and (not (featurep 'x-symbol-autoloads))
 	     ;; try requiring it
 	     (not (condition-case ()
-		      (require 'x-symbol) ;; NB: lose any errors!
+		      (require 'x-symbol) ;; NB: lose all errors!
 		    (t (featurep 'x-symbol)))))
 	(funcall error-or-warn
  "Proof General: x-symbol package must be installed for x-symbol-support!
@@ -88,34 +60,72 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
        ;;
        ;; Now check proof assistant has support provided
        ;;
-       ((or 
-	 (not (boundp xs-modes))
-	 ;; FIXME: add here a test that we can find file
-	 ;; x-symbol-<xs-lang>.el but maybe let x-symbol-load it.
-	 ;; [might be okay to do condition-case require as above]
-	 )
-	(funcall error-or-warn
+       ;; FIXME: maybe we should let x-symbol load the feature, in
+       ;; case it uses x-symbol stuff inside.
+       ;; Is there an easy way of testing for library exists?
+       ((not (condition-case ()
+		 (require xs-feature-sym) ;; NB: lose all errors!
+	       (t (featurep xs-feature-sym))))
  (format
-  "Proof General: for x-symbol support, you must set %s."
-  (symbol-name xs-modes))))
+  "Proof General: for x-symbol support, you must provide a library %s.el"
+  xs-feature))
        (t
 	;;
 	;; We've got everything we need!   So initialize.
 	;; 
-	(x-symbol-initialize)    ;; No harm in doing this multiple times
-	(x-symbol-register-language xs-lang xs-feature (eval xs-modes))
-	(push am-entry x-symbol-auto-mode-alist)
-	;; Font lock support is optional
-	(if (boundp sym-flks)
-	    (put symmode 'font-lock-defaults (list sym-flks)))
-	;;
-	;; Finished.
-	(setq proof-x-symbol-initialized t))))))
+	(let*
+	    ((xs-lang	     proof-assistant-symbol)
+	     (xs-xtra-modes  proof-xsym-extra-modes)
+	     (xs-std-modes   (list
+			      ;; NB: there is a problem with
+			      ;; initialization order here, these
+			      ;; variables are set in script/shell mode
+			      ;; initialization.  They ought to be set
+			      ;; earlier, and enforced as part of the
+			      ;; generic scheme.  For the time being,
+			      ;; we use default constructed names
+			      ;; [which every prover should follow]
+			      (or proof-mode-for-shell
+				  (intern (concat assistant "-shell-mode")))
+			      (or proof-mode-for-response
+				  (intern (concat assistant "-response-mode")))
+			      (or proof-mode-for-script
+				  ;; FIXME: next one only correct for isabelle
+				  (intern (concat assistant "-proofscript-mode")))
+			      (or  proof-mode-for-pbp
+				   (intern (concat assistant "-pbp-mode")))))
+	     (all-xs-modes   (append xs-std-modes xs-xtra-modes))
+	     (am-entry       (list proof-xsym-extra-modes t xs-lang))
+	     (symmode-nm     (concat assistant "sym-mode"))
+	     (symmode        (intern symmode-nm))
+	     (symnamevar     (intern (concat xs-feature "-name")))
+	     (symname	     (concat proof-assistant " Symbols"))
+	     (symmodelinevar (intern (concat xs-feature "-modeline-name")))
+	     (symmodelinenm  assistant)
+	     (flks	     proof-xsym-font-lock-keywords))
+
+
+	  (x-symbol-initialize)    ;; No harm in doing this multiple times
+	  ;; Set default name and modeline indicator for the symbol
+	  ;; minor mode
+	  (set symnamevar symname)
+	  (set symmodelinevar symmodelinenm)
+	  (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes)
+	  ;; Put just the extra modes on the auto-mode-alist
+	  (if xs-xtra-modes (push am-entry x-symbol-auto-mode-alist))
+	  ;; Font lock support is optional
+	  (if flks
+	      (put symmode 'font-lock-defaults (list flks)))
+	  ;;
+	  ;; 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))
+  (if ;(and proof-x-symbol-enable (not proof-x-symbol-initialized))
+      proof-x-symbol-enable
       (progn
 	(setq proof-x-symbol-enable nil) ; assume failure!
 	(proof-x-symbol-initialize 'giveerrors)
@@ -157,21 +167,20 @@ A value for proof-shell-insert-hook."
     (if proof-x-symbol-initialized
 	(progn
 	  (setq x-symbol-language proof-assistant-symbol)
-	  (if (eq x-symbol-mode 
-		  (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.
-	  (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
-
-
+	  (if (eq x-symbol-mode (not proof-x-symbol-enable))
+	      ;; toggle x-symbol-mode
+	      (x-symbol-mode))
+	  ;; 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)))
+	      (if (not font-lock-mode)
+		  (font-lock-mode)
+		;; Even if font-lock was on before we may need
+		;; to refontify now that the patterns (and buffer
+		;; contents) have changed. I think x-symbol
+		;; ought to do this really!
+		(font-lock-fontify-buffer)))))))
+	  
 (defun proof-x-symbol-mode-all-buffers ()
   "Activate/deactivate x-symbol mode in all Proof General buffers.
 A subroutine of proof-x-symbol-enable."
diff --git a/generic/proof.el b/generic/proof.el
index 90813468..95e70c07 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -238,11 +238,7 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
       (insert str) 
       (proof-x-symbol-decode-region start (point))
       (setq end (point-max))
-      (save-excursion
-	(font-lock-set-defaults)		;required for FSF Emacs 20.2
-;; FIXME da: does this break anything in LEGO or others?
-;DvO	(font-lock-fontify-region start end)
-	(if face (font-lock-append-text-property start end 'face face)))
+      (if face (font-lock-append-text-property start end 'face face))
       (buffer-substring start end))))
 
 ;; FIXME da: this window dedicated stuff is a real pain and I've