Extensive fixes for x-symbol and font-lock.

11 files changed, 229 insertions, 145 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index ce0aa189..cf38c25d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2481,6 +2481,7 @@ contents of that file.
 * Goals buffer settings::  
 * Global constants::            
 * Handling multiple files::     
+* Configuring X-Symbol::
 @end menu
 
 
@@ -3376,6 +3377,52 @@ for a automatic approximation to multiple file handling.
 
 
 
+@node Configuring X-Symbol::
+@section Configuring X-Symbol::
+@cindex X-Symbol
+
+The X-Symbol package (by Christoph Wedler) displays characters from a
+variety of fonts in Emacs buffers, automatically converting between
+codes for special characters and @i{tokens} which are character
+sequences stored in files.
+
+Proof General can use X-Symbol to allow interaction between the user and
+the proof assistant to use tokens, yet appear to be using special
+characters.  So proof scripts and proofs themselves can be processed
+with non-ascii characters for mathematical symbols.
+
+To configure X-Symbol for Proof General, you must understand a little
+bit of how X-Symbol works: read the documentation that is supplied with
+it.  The basic task is to set up a @i{token language} for your proof
+assistant.  If your assistant is stored in the subdirectory
+@var{myprover}, the token language will be called @var{myprover} and be
+defined in a file @file{x-symbol-@var{myprover}.el} which is
+automatically loaded by X-Symbol.  The name of the token language mode
+will be @code{@var{myprover}sym}.
+
+In the usual configuration file @file{@var{myprover}.el}, you must set
+several variables that Proof General uses to configure X-Symbol with.
+
+@c FIXME: more here!! unfinished!!
+
+@code{@var{myprover}sym-font-lock-keywords}
+
+@c TEXI DOCSTRING MAGIC: proof-xsym-activate-command
+
+@c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command
+
+We expect tokens to be used uniformly, so that along with each script
+mode buffer, the response buffer, goals buffer, and shell buffer are all
+kept in X-Symbol minor mode to display special characters.  This happens
+automatically.  If you want additional modes, you can set 
+@code{proof-xsym-extra-modes}.
+
+@c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes
+
+
+
+
+
 @node Internals of Proof General
 @chapter Internals of Proof General
 
diff --git a/etc/junk.el b/etc/junk.el
index 41e47db6..46da7f0c 100644
--- a/etc/junk.el
+++ b/etc/junk.el
@@ -32,3 +32,28 @@ arrive."
 	      'proof-eager-annotation-face))
     (proof-shell-message str))))
 
+
+;  (cond
+;   ((string-match "FSF" emacs-version)
+;    ;; 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)))
+;   ;; In XEmacs, we must make a new variable to hold
+;   ;; the defaults.  
+;   ;; (FIXME: this makes toggling font-lock robust now, before
+;   ;;  it was ropy.  Should check whether this is the right
+;   ;;  was for FSF too).
+;   (t
+;    (let
+;	((flks	(intern (concat (symbol-name major-mode)
+;				"-font-lock-defaults"))))
+;      ;; Take a copy of current font-lock-keywords to make them
+;      ;; the default in future.  Then font-lock-mode can be
+;      ;; safely switched on and off.
+;      (set flks font-lock-keywords)
+;      (make-local-variable 'proof-font-lock-defaults)
+;      (setq proof-font-lock-defaults font-lock-keywords)
+;      (setq font-lock-defaults '(proof-font-lock-defaults)))))
+      ; (put major-mode 'font-lock-defaults (list flks)))))
+
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
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 861b6082..767df53a 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -297,7 +297,7 @@
    (cons (concat "\353\\?'" isa-idx "\350") 'isabelle-tvar-name-face)
    (cons (concat "\354" isa-id "\350") 'isabelle-free-name-face)
    (cons (concat "\355" isa-id "\350") 'isabelle-bound-name-face)
-   (cons (concat "\356" isa-idx "\350") 'isabelle-var-name-face)
+   (cons (concat "\356" "\\?" isa-idx "\350") 'isabelle-var-name-face)
    (cons (concat "\357" isa-idx "\350") 'proof-declaration-name-face)
    )
   "*Font-lock table for Isabelle terms.")
diff --git a/isa/isa.el b/isa/isa.el
index 849014c5..03cfaf22 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -313,7 +313,7 @@ proof-shell-retract-files-regexp."
 
 (eval-and-compile			; to define vars for byte comp.
 (define-derived-mode isa-pbp-mode pbp-mode
-  "Isabelle proofstate" nil
+  "Isabelle goals" nil
   (isa-pbp-mode-config)))
 
 (eval-and-compile			; to define vars for byte comp.
@@ -650,29 +650,16 @@ you will be asked to retract the file or process the remainder of it.
 ;; x-symbol support for Isabelle PG, provided by David von Oheimb.
 ;;
 ;; The following settings configure the generic PG package.
-;;
 ;; The token language "Isabelle Symbols" is in file x-symbol-isa.el
 ;;
 
-;; name of minor isa mode
-(defvar x-symbol-isa-name "Isabelle Symbols")
-
-(defvar x-symbol-isa-modes 
-  '(isasym-mode 
-    isa-proofscript-mode 
-    proof-response-mode			; should be isa-response-mode?
-    proofstate-mode			; isa-proofstate-mode?
-    isa-shell-mode 
-    isa-pbp-mode
-    thy-mode				; necessary?
-    isa-thy-mode
-    shell-mode				; necessary?
-    ))
-
-(defvar isasym-font-lock-keywords
-  '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))))
-
-(setq proof-xsym-activate-command
+(setq proof-xsym-extra-modes
+      '(isasym-mode ; necessary?
+	thy-mode
+	shell-mode) ; necessary?
+      proof-xsym-font-lock-keywords
+      '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face)))
+      proof-xsym-activate-command
       "print_mode := (!print_mode union [\"xsymbols\",\"symbols\"])"
       proof-xsym-deactivate-command
       "print_mode := filter_out (fn x=>(rev (explode \"symbols\") prefix rev (explode x))) (!print_mode)")
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
index d0cfbf81..5c38ced8 100644
--- a/isa/x-symbol-isa.el
+++ b/isa/x-symbol-isa.el
@@ -6,8 +6,6 @@
 (provide 'x-symbol-isa)
 (defvar x-symbol-isa-required-fonts nil)
 
-;(defvar x-symbol-isa-name "Isabelle Symbol")
-(defvar x-symbol-isa-modeline-name "isa")
 (defvar x-symbol-isa-header-groups-alist nil)
 ;'(("Operator" bigop operator)
 ;    ("Relation" relation)
diff --git a/todo b/todo
index 23f2874e..9c8909fe 100644
--- a/todo
+++ b/todo
@@ -52,6 +52,9 @@ re-enabled), proof-toggle-scripting, new configuration options.
     - noticeable delay when loading ML files for Isabelle (fontification?)
     - clean up assert-until-point stuff at last!
 
+B Have seen "confused" bug: shows up when do lots of C-c C-n as
+  process is starting up.
+
 D Why don't PG's minor modes appear on XEmacs minor mode menu?
   (C-right on status bar)
 
@@ -60,11 +63,6 @@ A Markus's bug reminder list:
   - c-c c-c does not work reliably;
   - c-c c-a is broken;
 
-A bug in response filtering:
-   The response filtering seems to have changed again.  E.g. 'Info' button in
-   PG/isar (without a theory context) omits most of the result (commands,
-   ...).
-
 A Bugs in x-symbol support: 
    - visiting multiple files sometimes doesn't display them properly
      (setq x-symbol-8bits nil) needed?