Merge changes from Version4Branch.

2 files changed, 156 insertions, 325 deletions

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index d7dc6fef..18f36906 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -29,7 +29,6 @@
 @c Some URLs.
 @c FIXME: unfortunately, broken in buggy pdftexinfo.
 @c so removed for now.
-@set URLxsymbol  http://x-symbol.sourceforge.net/
 @set URLisamode  http://homepages.inf.ed.ac.uk/da/isamode
 @set URLpghome   http://proofgeneral.inf.ed.ac.uk
 @set URLpglatestrpm  http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest.noarch.rpm
@@ -181,7 +180,7 @@ Proof General.
 * Handling Multiple Files::     
 * Configuring Editing Syntax::
 * Configuring Font Lock::
-* Configuring X-Symbol::
+* Configuring Tokens::
 * Writing More Lisp Code::
 * Internals of Proof General::  
 * Plans and Ideas::             
@@ -636,7 +635,7 @@ the standard Proof General buttons.
 Here's an example of how to remove a button, from @file{af2.el}:
 @lisp
 (setq af2-toolbar-entries
-      (remassoc 'state af2-toolbar-entries))
+      (assq-delete-all 'state af2-toolbar-entries))
 @end lisp
 
 
@@ -751,7 +750,7 @@ as well as @samp{@code{proof-script-comment-end}}.
 @defvar proof-script-comment-start-regexp 
 Regexp which matches a comment start in the proof command language.
 
-The default value for this is set as (@code{regexp-quote} @code{proof-script-comment-start})
+The default value for this is set as (@code{regexp-quote} @samp{@code{proof-script-comment-start}})
 but you can set this variable to something else more precise if necessary.
 @end defvar
 
@@ -780,7 +779,7 @@ but you can set this variable to something else more precise if necessary.
 Value for @samp{@code{case-fold-search}} when recognizing portions of proof scripts.@*
 Also used for completion, via @samp{@code{proof-script-complete}}.
 The default value is nil.  If your prover has a case @strong{insensitive}
-input syntax, @code{proof-case-fold-search} should be set to t instead.
+input syntax, @samp{@code{proof-case-fold-search}} should be set to t instead.
 NB: This setting is not used for matching output from the prover.
 @end defvar
 
@@ -815,10 +814,10 @@ for @samp{@code{proof-script-next-entity-regexps}} used for function menus.
 @defvar proof-goal-command-p 
 A function to test: is this really a goal command span?
 
-This is added as a more refined addition to @code{proof-goal-command-regexp},
+This is added as a more refined addition to @samp{@code{proof-goal-command-regexp}},
 to solve the problem that Coq and some other provers can have goals which
 look like definitions, etc.  (In the future we may generalize
-@code{proof-goal-command-regexp} instead).
+@samp{@code{proof-goal-command-regexp}} instead).
 @end defvar
 
 
@@ -826,7 +825,7 @@ look like definitions, etc.  (In the future we may generalize
 @defvar proof-goal-with-hole-regexp 
 Regexp which matches a command used to issue and name a goal.@*
 The name of the theorem is built from the variable
-@code{proof-goal-with-hole-result} using the same convention as
+@samp{@code{proof-goal-with-hole-result}} using the same convention as
 for @samp{@code{query-replace-regexp}}.
 Used for setting names of goal..save regions and for default
 configuration of other modes (function menu, imenu).
@@ -837,9 +836,9 @@ It's safe to leave this setting as nil.
 @c TEXI DOCSTRING MAGIC: proof-goal-with-hole-result
 @defvar proof-goal-with-hole-result 
 How to build theorem name after matching with @samp{@code{proof-goal-with-hole-regexp}}.@*
-String or Int. 
-If an int N use @code{match-string} to recover the value of the Nth parenthesis matched. 
-If it is a string use @code{replace-match}. In this case, @code{proof-save-with-hole-regexp} 
+String or Int.
+If an int N use @code{match-string} to recover the value of the Nth parenthesis matched.
+If it is a string use @code{replace-match}. In this case, @code{proof-save-with-hole-regexp}
 should match the entire command
 @end defvar
 
@@ -888,12 +887,9 @@ save commands, so don't use that if your prover has save commands.
 @defvar proof-really-save-command-p 
 Is this really a save command?
 
-This is a more refined addition to @code{proof-save-command-regexp}.
+This is a more refined addition to @samp{@code{proof-save-command-regexp}}.
 It should be a function taking a span and command as argument,
-and can be used to track nested proofs.  (See what is done in
-isar/ for example).  In the future, this setting should be
-removed when the generic core is extended to handle nested
-proofs smoothly.
+and can be used to track nested proofs.
 @end defvar
 
 
@@ -1001,8 +997,8 @@ only at the end.  However, it does not parse strings,
 comments, or parentheses.
 
 This variable may not need to be set: a default value which should
-work for goal..saves is calculated from @code{proof-goal-with-hole-regexp},
-@code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}.
+work for goal..saves is calculated from @samp{@code{proof-goal-with-hole-regexp}},
+@samp{@code{proof-goal-command-regexp}}, and @samp{@code{proof-save-with-hole-regexp}}.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn
@@ -1018,7 +1014,7 @@ cell of the name and the beginning of the entity's region.
 
 Note that @samp{@code{proof-script-next-entity-regexps}} is set to a default value
 from @samp{@code{proof-goal-with-hole-regexp}} and @samp{@code{proof-save-with-hole-regexp}} in
-the function @code{proof-config-done}, so you may not need to worry about any
+the function @samp{@code{proof-config-done}}, so you may not need to worry about any
 of this.  See whether function menu does something sensible by
 default.
 @end defvar
@@ -1099,7 +1095,7 @@ It should undo the effect of all settings between its target span
 up to (@code{proof-locked-end}).  This may involve forgetting a number
 of definitions, declarations, or whatever.
 
-The special string @code{proof-no-command} means there is nothing to do.
+The special string @samp{@code{proof-no-command}} means there is nothing to do.
 
 This is an important function for script management.
 Study one of the existing instantiations for examples of how to write it,
@@ -1148,7 +1144,7 @@ will be attempted.
 @defvar proof-kill-goal-command 
 Command to kill the currently open goal.
 
-If this is set to nil, PG will expect @code{proof-find-and-forget-fn}
+If this is set to nil, PG will expect @samp{@code{proof-find-and-forget-fn}}
 to do all the work of retracting to an arbitrary point in a file.
 Otherwise, the generic split-phase mechanism will be used:
 
@@ -1210,7 +1206,7 @@ assistant (with respect to an on-going proof).
 @c TEXI DOCSTRING MAGIC: proof-state-preserving-p
 @defvar proof-state-preserving-p 
 A predicate, non-nil if its argument (a command) preserves the proof state.@*
-This is a safety-test used by @code{proof-minibuffer-cmd} to filter out scripting
+This is a safety-test used by @samp{@code{proof-minibuffer-cmd}} to filter out scripting
 commands which should be entered directly into the script itself.
 
 The default setting for this function, @samp{@code{proof-generic-state-preserving-p}}
@@ -1239,7 +1235,7 @@ script).
 
 When functions in this hook are called, the variable
 @samp{activated-interactively} will be non-nil if
-@code{proof-activate-scripting} was called interactively
+@samp{@code{proof-activate-scripting}} was called interactively
 (rather than as a side-effect of some other action).
 If a hook function sends commands to the proof process,
 it should wait for them to complete (so the queue is cleared
@@ -1352,7 +1348,7 @@ to send to the prover to activate certain actions.
 System command to run the proof assistant in the proof shell.@*
 May contain arguments separated by spaces, but see also @samp{proof-prog-args}.
 
-Remark: if @samp{proof-prog-args} is non-nil, then @code{proof-prog-name} is considered
+Remark: if @samp{proof-prog-args} is non-nil, then @samp{@code{proof-prog-name}} is considered
 strictly: it must contain @strong{only} the program name with no option, spaces
 are interpreted literally as part of the program name.
 @end defvar
@@ -1362,8 +1358,8 @@ are interpreted literally as part of the program name.
 Non-nil if Proof General should try to add terminator to every command.@*
 If non-nil, whenever a command is sent to the prover using
 @samp{@code{proof-shell-invisible-command}}, Proof General will check to see if it
-ends with @code{proof-terminal-char}, and add it if not.
-If @code{proof-terminal-char} is nil, this has no effect.
+ends with @samp{@code{proof-terminal-char}}, and add it if not.
+If @samp{@code{proof-terminal-char}} is nil, this has no effect.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd
@@ -1403,7 +1399,7 @@ A command to quit the proof process.  If nil, send EOF instead.
 
 @c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout
 @defvar proof-shell-quit-timeout 
-The number of seconds to wait after sending @code{proof-shell-quit-cmd}.@*
+The number of seconds to wait after sending @samp{@code{proof-shell-quit-cmd}}.@*
 After this timeout, the proof shell will be killed off more rudely.
 If your proof assistant takes a long time to clean up (for
 example writing persistent databases out or the like), you may
@@ -1417,12 +1413,12 @@ The format character @samp{%s} is replaced with the directory, and
 the escape sequences in @samp{@code{proof-shell-filename-escapes}} are
 applied to the filename.
 
-This setting is used to define the function @code{proof-cd} which
+This setting is used to define the function @samp{@code{proof-cd}} which
 changes to the value of (@code{default-directory}) for script buffers.
 For files, the value of (@code{default-directory}) is simply the
 directory the file resides in.
 
-NB: By default, @code{proof-cd} is called from @code{proof-activate-scripting-hook},
+NB: By default, @samp{@code{proof-cd}} is called from @samp{@code{proof-activate-scripting-hook}},
 so that the prover switches to the directory of a proof
 script every time scripting begins.
 @end defvar
@@ -1432,7 +1428,7 @@ script every time scripting begins.
 Command to turn prover goals output off when sending many script commands.@*
 If non-nil, Proof General will automatically issue this command
 to help speed up processing of long proof scripts.
-See also @code{proof-shell-stop-silent-cmd}.
+See also @samp{@code{proof-shell-stop-silent-cmd}}.
 NB: terminator not added to command.
 @end defvar
 
@@ -1441,7 +1437,7 @@ NB: terminator not added to command.
 Command to turn prover output on.@*
 If non-nil, Proof General will automatically issue this command
 to help speed up processing of long proof scripts.
-See also @code{proof-shell-start-silent-cmd}.
+See also @samp{@code{proof-shell-start-silent-cmd}}.
 NB: Terminator not added to command.
 @end defvar
 
@@ -1473,8 +1469,8 @@ issuing this command.
 
 If this is set to nil, no command is issued.
 
-See also: @code{proof-shell-inform-file-retracted-cmd},
-@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
+See also: @samp{@code{proof-shell-inform-file-retracted-cmd}},
+@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd
 @defvar proof-shell-inform-file-retracted-cmd 
@@ -1500,8 +1496,8 @@ be invoked on the name of the retracted file, and should remove
 the ancestor files from @samp{@code{proof-included-files-list}} by some
 other calculation.
 
-See also: @code{proof-shell-inform-file-processed-cmd},
-@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}.
+See also: @samp{@code{proof-shell-inform-file-processed-cmd}},
+@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}.
 @end defvar
 
 
@@ -1534,10 +1530,10 @@ Can be used to configure the proof assistant to the interface in
 various ways -- for example, to observe or alter the commands sent to
 the prover, or to sneak in extra commands to configure the prover.
 
-This hook is called inside a @samp{@code{save-excursion}} with the @code{proof-shell-buffer}
+This hook is called inside a @samp{@code{save-excursion}} with the @samp{@code{proof-shell-buffer}}
 current, just before inserting and sending the text in the
 variable @samp{string}.  The hook can massage @samp{string} or insert additional
-text directly into the @code{proof-shell-buffer}.
+text directly into the @samp{@code{proof-shell-buffer}}.
 Before sending @samp{string}, it will be stripped of carriage returns.
 
 Additionally, the hook can examine the variable @samp{action}.  It will be
@@ -1563,8 +1559,6 @@ Example uses:
 @var{lego} uses this hook for setting the pretty printer width if
 the window width has changed;
 Plastic uses it to remove literate-style markup from @samp{string}.
-The x-symbol support uses this hook to convert special characters
-into tokens for the proof assistant.
 @end defvar
 
 
@@ -1614,7 +1608,7 @@ recognize when the prover has finished processing a command.
 To help speed up matching you may be able to annotate the
 proof assistant prompt with a special character not appearing
 in ordinary output.  The special character should appear in
-this regexp, and should be the value of @code{proof-shell-wakeup-char}.
+this regexp, and should be the value of @samp{@code{proof-shell-wakeup-char}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-abort-goal-regexp
 @defvar proof-shell-abort-goal-regexp 
@@ -1627,15 +1621,15 @@ Regexp matching an error report from the proof assistant.
 We assume that an error message corresponds to a failure in the last
 proof command executed.  So don't match mere warning messages with
 this regexp.  Moreover, an error message should not be matched as an
-eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it
+eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it
 will be lost.
 
-Error messages are considered to begin from @code{proof-shell-error-regexp}
+Error messages are considered to begin from @samp{@code{proof-shell-error-regexp}}
 and continue until the next prompt.  The variable
 @samp{@code{proof-shell-truncate-before-error}} controls whether text before the
 error message is displayed.
 
-The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}.
+The engine matches interrupts before errors, see @samp{@code{proof-shell-interrupt-regexp}}.
 
 It is safe to leave this variable unset (as nil).
 @end defvar
@@ -1645,10 +1639,10 @@ Regexp matching output indicating the assistant was interrupted.@*
 We assume that an interrupt message corresponds to a failure in the last
 proof command executed.  So don't match mere warning messages with
 this regexp.  Moreover, an interrupt message should not be matched as an
-eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it
+eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it
 will be lost.
 
-The engine matches interrupts before errors, see @code{proof-shell-error-regexp}.
+The engine matches interrupts before errors, see @samp{@code{proof-shell-error-regexp}}.
 
 It is safe to leave this variable unset (as nil).
 @end defvar
@@ -1659,9 +1653,9 @@ Non-nil means truncate output that appears before error messages.@*
 If nil, the whole output that the prover generated before the last
 error message will be shown.
 
-NB: the default setting for this is @samp{t} to be compatible with
+NB: the default setting for this is t to be compatible with
 behaviour in Proof General before version 3.4.  The more obvious
-setting for new instances is probably @samp{nil}.
+setting for new instances is probably nil.
 
 Interrupt messages are treated in the same way.
 See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt-regexp}}.
@@ -1689,7 +1683,7 @@ and possibly analysed further for proof-by-pointing markup.
 @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp
 @defvar proof-shell-end-goals-regexp 
 Regexp matching the end of the proof state output, or nil.@*
-If nil, just use the rest of the output following @code{proof-shell-start-goals-regexp}.
+If nil, just use the rest of the output following @samp{@code{proof-shell-start-goals-regexp}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp
 @defvar proof-shell-assumption-regexp 
@@ -1724,7 +1718,7 @@ Eager annotation field start.  A regular expression or nil.@*
 An "eager annotation indicates" to Proof General that some following output
 should be displayed (or processed) immediately and not accumulated for
 parsing later.  Note that this affects processing of output which is
-ordinarily accumulated: output which appears before the eager annotation 
+ordinarily accumulated: output which appears before the eager annotation
 start will be discarded.
 
 The start/end annotations can be used to hilight the output, but
@@ -1806,7 +1800,7 @@ A good markup for the second string is to delimit with #'s, since
 these are not valid syntax for elisp evaluation.
 
 Elisp errors will be trapped when evaluating; set
-@code{proof-general-debug} to be informed when this happens.
+@samp{@code{proof-general-debug}} to be informed when this happens.
 
 Example uses are to adjust PG's internal copies of proof assistant's
 settings, or to make automatic dynamic syntax adjustments in Emacs to
@@ -1959,8 +1953,8 @@ Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to
 determine whether the cause was an error or interrupt.  Possible
 values for this hook include:
 @lisp
- @code{proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window}
- @code{proof-goto-end-of-locked-if-pos-not-visible-in-window}
+ @samp{@code{proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window}}
+ @samp{@code{proof-goto-end-of-locked-if-pos-not-visible-in-window}}
 @end lisp
 which move the cursor in the scripting buffer on an error or
 error/interrupt.
@@ -1971,8 +1965,8 @@ something in scripting buffer, @samp{@code{save-excursion}} and/or @samp{@code{s
 
 @c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook
 @defvar proof-shell-pre-interrupt-hook 
-Run immediately after @samp{@code{comint-interrupt-subjob}} is called.  This@*
-hook is added to allow customization for systems that query the user
+Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@*
+This hook is added to allow customization for systems that query the user
 before returning to the top level.
 @end defvar
 
@@ -2014,13 +2008,13 @@ at how to use these settings.
 @defvar pg-goals-change-goal 
 Command to change to the goal @samp{%s}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: pbp-goal-command
+@c TEXI FIX DOCSTRING MAGIC: pbp-goal-command
 @defvar pbp-goal-command 
-Command sent when @samp{@code{pg-goals-button-action}} is requested on a goal.
+Command sent when @samp{pg-goals-button-action} is requested on a goal.
 @end defvar
-@c TEXI DOCSTRING MAGIC: pbp-hyp-command
+@c TEXI FIX DOCSTRING MAGIC: pbp-hyp-command
 @defvar pbp-hyp-command 
-Command sent when @samp{@code{pg-goals-button-action}} is requested on an assumption.
+Command sent when @samp{pg-goals-button-action} is requested on an assumption.
 @end defvar
 @c TEXI DOCSTRING MAGIC: pg-goals-error-regexp
 @defvar pg-goals-error-regexp 
@@ -2041,13 +2035,13 @@ In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-c
 @defvar pg-subterm-start-char 
 Opening special character for subterm markup.@*
 Subsequent special characters with values @strong{below}
-@code{pg-subterm-first-special-char} are assumed to be subterm position
-indicators.  Annotations should be finished with @code{pg-subterm-sep-char}; 
-the end of the concrete syntax is indicated by @code{pg-subterm-end-char}.
+@samp{@code{pg-subterm-first-special-char}} are assumed to be subterm position
+indicators.  Annotations should be finished with @samp{@code{pg-subterm-sep-char}}; 
+the end of the concrete syntax is indicated by @samp{@code{pg-subterm-end-char}}.
 
 If @samp{@code{pg-subterm-start-char}} is nil, subterm markup is disabled.
 
-See doc of @samp{@code{pg-assoc-analyse-structure}} for more details of
+See doc of @samp{pg-assoc-analyse-structure} for more details of
 subterm and proof-by-pointing markup mechanisms..
 @end defvar
 @c TEXI DOCSTRING MAGIC: pg-subterm-sep-char
@@ -2363,38 +2357,23 @@ Proof General, @pxref{Demonstration instance and easy configuration}.
 @c TEXI DOCSTRING MAGIC: proof-script-font-lock-keywords
 @defvar proof-script-font-lock-keywords 
 Value of @samp{@code{font-lock-keywords}} used to fontify proof scripts.@*
-This is currently used only by @samp{@code{proof-easy-config}} mechanism,
-to set @samp{@code{font-lock-keywords}} before calling @code{proof-config-done}.
-See also proof-@{shell,resp,goals@}-@code{font-lock-keywords}.
-@end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-font-lock-keywords
-@defvar proof-shell-font-lock-keywords 
-Value of @samp{@code{font-lock-keywords}} used to fontify the proof shell.@*
-This is currently used only by @samp{@code{proof-easy-config}} mechanism, to set
-@samp{@code{font-lock-keywords}} before calling @samp{@code{proof-config-done}}.
-See also proof-@{script,resp,goals@}-@code{font-lock-keywords}.
+The proof script mode should set this before calling @samp{@code{proof-config-done}}.
+Used also by @samp{@code{proof-easy-config}} mechanism.
+See also proof-@{resp,goals@}-@code{font-lock-keywords}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-goals-font-lock-keywords
 @defvar proof-goals-font-lock-keywords 
 Value of @samp{@code{font-lock-keywords}} used to fontify the goals output.@*
-NB: the goals output is not kept in font lock mode because the
-fontification may rely on annotations which are erased before
-displaying.  This means internal functions of PG must be used
-to display to the goals buffer to ensure fontification is done!
-This is currently used only by @samp{@code{proof-easy-config}} mechanism,
-to set @samp{@code{font-lock-keywords}} before calling @code{proof-config-done}.
-See also proof-@{script,shell,resp@}-@code{font-lock-keywords}.
+The goals shell mode should set this before calling @samp{@code{proof-goals-config-done}}.
+Used also by @samp{@code{proof-easy-config}} mechanism.
+See also @samp{proof-@{script,goals@}-@code{font-lock-keywords}}.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-resp-font-lock-keywords
 @defvar proof-resp-font-lock-keywords 
 Value of @samp{@code{font-lock-keywords}} used to fontify the response output.@*
-NB: the goals output is not kept in font lock mode because the
-fontification may rely on annotations which are erased before
-displaying.  This means internal functions of PG must be used
-to display to the goals buffer to ensure fontification is done!
-This is currently used only by @code{proof-easy-config} mechanism,
-to set @code{font-lock-keywords} before calling @code{proof-config-done}.
-See also proof-@{script,shell,resp@}-@code{font-lock-keywords}.
+The response mode should set this before calling @samp{@code{proof-response-config-done}}.
+Used also by @samp{@code{proof-easy-config}} mechanism.
+See also @samp{proof-@{script,goals@}-@code{font-lock-keywords}}.
 @end defvar
 Proof General provides a special function, @code{proof-zap-commas}, for
 tweaking the font lock behaviour of provers which have declarations of
@@ -2426,63 +2405,45 @@ This hook is called before fonfitying a region in an output buffer.@*
 
 
 
-@node Configuring X-Symbol
-@chapter Configuring X-Symbol
+@node Configuring Tokens
+@chapter Configuring Tokens
 @cindex X-Symbol
+@cindex Unicode Tokens
+@cindex Tokens
 
-The X-Symbol package is described in the Proof General user manual.  To
-configure X-Symbol for Proof General, you must understand a little bit
+The Tokens package is described in the Proof General user manual.  To
+configure Tokens 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}.
-
-Proof General will check that the file @file{x-symbol-@var{myprover}.el}
-exists and set up X-Symbol to load it.  The token language file must
-define a number of standard settings, and X-Symbol will give warnings if
-any of them are missing.
-
-Apart from the token language file, there are several settings for
-X-Symbol which you can set in the usual configuration file
-@file{@var{myprover}.el}.  These settings are optional.
-
-@c There's also proof-xsym-font-lock-keywords, but I don't 
-@c really know what this setting is good for.
-
-@c TEXI DOCSTRING MAGIC: proof-xsym-activate-command
-@defvar proof-xsym-activate-command 
-Command to activate token input/output for X-Symbol.@*
+@c TEXI DOCSTRING MAGIC: proof-tokens-activate-command
+@defvar proof-tokens-activate-command 
+Command to activate token input/output for prover.@*
 If non-nil, this command is sent to the proof assistant when
-X-Symbol support is activated.
+Unicode Tokens support is activated.
 @end defvar
-
-@c TEXI DOCSTRING MAGIC: proof-xsym-deactivate-command
-@defvar proof-xsym-deactivate-command 
-Command to deactivate token input/output for X-Symbol.@*
+@c TEXI DOCSTRING MAGIC: proof-tokens-deactivate-command
+@defvar proof-tokens-deactivate-command 
+Command to deactivate token input/output for prover.@*
 If non-nil, this command is sent to the proof assistant when
-X-Symbol support is deactivated.
+Unicode Tokens support is deactivated.
 @end defvar
-
 We expect tokens to be used uniformly, so that along with each script
-mode buffer, the response buffer and goals buffer also invoke X-Symbol
+mode buffer, the response buffer and goals buffer also invoke Tokens
 to display special characters in the same token language.  This happens
-automatically.  If you want additional modes to use X-Symbol with the
+automatically.  If you want additional modes to use Tokens with the
 token language for your proof assistant, you can set
-@code{proof-xsym-extra-modes}.
+@code{proof-tokens-extra-modes}.
 
-@c TEXI DOCSTRING MAGIC: proof-xsym-extra-modes
-@defvar proof-xsym-extra-modes 
-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,
+@c TEXI DOCSTRING MAGIC: proof-tokens-extra-modes
+@defvar proof-tokens-extra-modes 
+List of additional mode names to use with Proof General tokens.@*
+These modes will have Tokens 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).
 @end defvar
+@end defvar
 
 
 
@@ -2914,14 +2875,14 @@ interfacing properly with the @code{customize} mechanism.
 
 @c TEXI DOCSTRING MAGIC: proof-set-value
 @defun proof-set-value sym value
-Set a customize variable using @code{set-default} and a function.@*
+Set a customize variable using @samp{@code{set-default}} and a function.@*
 We first call @samp{@code{set-default}} to set @var{sym} to @var{value}.
 Then if there is a function @var{sym} (i.e. with the same name as the
 variable @var{sym}), it is called to take some dynamic action for the new
 setting.
 
 If there is no function @var{sym}, we try stripping
-@code{proof-assistant-symbol} and adding "proof-" instead to get
+@samp{@code{proof-assistant-symbol}} and adding "proof-" instead to get
 a function name.  This extends @code{proof-set-value} to work with
 generic individual settings.
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 9ef284df..01186d0a 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -70,8 +70,7 @@
 @c        @ref{node}                without "see". Careful for info.
 @c
 
-@set version 3.7
-@set xemacsversion 21.5.28
+@set version 4.0pre
 @set fsfversion 22.2.1
 @set last-update July 2008
 @set rcsid $Id$
@@ -170,10 +169,10 @@ Visit Proof General on the web at @code{http://proofgeneral.inf.ed.ac.uk}
 This file documents version @value{version} of @b{Proof General}, a
 generic Emacs interface for proof assistants.
 
-Proof General @value{version} has been tested with XEmacs
-@value{xemacsversion} and GNU Emacs @value{fsfversion}.  It is supplied
-ready to use for the proof assistants LEGO, Coq, Isabelle, and PhoX.
-Experimental support is provided for several other provers.
+Proof General @value{version} has been tested with GNU Emacs
+@value{fsfversion} on Linux.  It is supplied ready to use for the proof
+assistants LEGO, Coq, Isabelle, and PhoX.  Experimental support is
+provided for several other provers.
 
 @menu
 * Preface::                     
@@ -245,11 +244,10 @@ Summer Schools.  Many new features have been added to enhance Coq mode
 Support has been added for the useful Emacs packages Speedbar
 @c @uref{http://cedet.sourceforge.net/speedbar.shtml,Speedbar} 
 and Index Menu, both usually distributed with Emacs.
-Compatible versions of the Emacs packages X-Symbol (for mathematical
-symbols in place of ASCII sequences), Math-Menu (for Unicode symbols)
+Compatible versions of the Emacs packages Math-Menu (for Unicode symbols)
 and MMM Mode (for multiple modes in one buffer) are 
 bundled with Proof General.  A new Unicode Tokens package has
-been added which will replace X-Symbol eventually.
+been added which replaces X-Symbol.
 
 @c The display handling functions have been improved to be more user
 @c friendly and the display in multiple-window mode is trimmed to
@@ -261,7 +259,6 @@ desktop integration on freedesktop.org compliant desktops (including,
 for example, many recent Linux distributions).
 
 @c Other stuff pending:
-@c X-Symbol 4.4 support??
 @c Support for *thms* buffer??
 
 See the @file{CHANGES} file in the distribution for more complete
@@ -1747,8 +1744,8 @@ cursor between buffers.
 The mouse bindings are these:
 
 @table @kbd
-@item button2
-@code{pg-goals-button-action}
+@c @item button2
+@c FIXME: @code{pg-goals-button-action}
 @item C-button2
 @code{proof-undo-and-delete-last-successful-command}
 @item button3
@@ -1771,7 +1768,7 @@ single step in the proof script.  However, if the proof is later
 replayed (without using PBP), the proof-by-pointing constructions will
 be considered as separate proof commands, as usual.
 
-@c TEXI DOCSTRING MAGIC: pg-goals-button-action
+@c TEXI FIXME DOCSTRING MAGIC: pg-goals-button-action
 @deffn Command pg-goals-button-action event
 Construct a proof-by-pointing command based on the mouse-click @var{event}.@*
 This function should be bound to a mouse button in the Proof General
@@ -1797,7 +1794,7 @@ The right-hand mouse button provides this convenient way to copy
 subterms from the goals buffer, using the function
 @code{pg-goals-yank-subterm}.
 
-@c TEXI DOCSTRING MAGIC: pg-goals-yank-subterm
+@c TEXI FIXME DOCSTRING MAGIC: pg-goals-yank-subterm
 @deffn Command pg-goals-yank-subterm event
 Copy the subterm indicated by the mouse-click @var{event}.@*
 This function should be bound to a mouse button in the Proof General
@@ -2241,7 +2238,6 @@ and @code{etags}.
 
 @menu
 * Syntax highlighting::         
-* X-Symbol support::
 * Unicode support::
 * Imenu and Speedbar (and Function Menu)::
 * Support for outline mode::    
@@ -2265,18 +2261,8 @@ specific portion of Proof General.  Moreover, Proof General usually
 decorates the output from the proof assistant, also using
 @code{font-lock}.
 
-In XEmacs, fontification is automatically turned on. To automatically
-switch on fontification in GNU Emacs 20.4, you may need to engage
-@code{M-x global-font-lock-mode}.  The old mechanism of adding hooks to
-the mode hooks (@code{lego-mode-hooks}, @code{coq-mode-hooks}, etc) is
-no longer recommended; it should not be needed in latest Emacs versions
-which have more flexible customization.
-
-Fontification for output is controlled by a separate switch in Proof
-General. Set @code{proof-output-fontify-enable} to @code{nil} if you
-don't want the output from your proof assistant to be fontified
-according to the setting of @code{font-lock-keywords} in the proof
-assistant specific portion of Proof General. @xref{User options}.
+To automatically switch on fontification in Emacs, you may need
+to engage @code{M-x global-font-lock-mode}.  
 
 By the way, the choice of colour, font, etc, for each kind of markup is
 fully customizable in Proof General.  Each @emph{face} (Emacs
@@ -2288,64 +2274,6 @@ Proof General -> Advanced -> Customize -> Faces -> Proof Faces.
 @end lisp
 
 
-@node X-Symbol support
-@section X-Symbol support
-@cindex symbols
-@cindex X-Symbols
-@cindex Greek letters
-@cindex logical symbols
-@cindex mathematical symbols
-
-The X-Symbol package 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 uses 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 can be processed with real
-mathematical symbols, Greek letters, etc.
-
-The X-Symbol package is now bundled with Proof General.  You will be
-able to enable X-Symbol support if support has been provided in Proof
-General for a token language for your proof assistant.  To
-enable X-Symbol, use the menu item:
-@example
-  Proof-General -> Options -> X-Symbol
-@end example
-To enable it automatically every time you use Proof General,
-just use
-@example
-  Proof-General -> Options -> Save Options
-@end example
-once it has been selected.  (Alternatively, customize the setting
-@code{@emph{PA}-x-symbol-enable}).
-
-You may also simply use @code{M-x x-symbol-mode} to turn on and off
-X-Symbol display in the scripting buffer, as you would when using
-X-Symbol for other modes, or indeed, as for any other Emacs minor mode.
-However, this way of turning on and off symbols will only affect the
-current script buffer, and will not change the status of any symbol
-configuration for the prover input/output (some proof assistants, such
-as Isabelle, have switches for enabling symbol output).  To make
-sure that symbol output is switched on or off for the prover
-as a whole, use the menu option mentioned above, or its underlying
-command, @code{M-x proof-x-symbol-toggle}.
-
-Notice that for proper symbol support, the proof assistant needs to have
-a special @i{token language}, or a special character set, to use
-symbols.  In this case, the proof assistant will output, and accept as
-input, tokens like @code{\longrightarrow}, which display as the
-corresponding symbols.  However, for proof assistants which do not have
-such token support, we can use "fake" symbol support quite effectively,
-displaying ordinary ASCII character sequences such as @code{-->} with
-symbols.  
-
-For more information about the X-Symbol package, please visit
-its home page at @uref{http://x-symbol.sourceforge.net/}.  
-
-@c @xref{Configuring X-Symbol}, for notes about how to configure
-@c a proof assistant to use X-Symbol in Proof General.
-
 @node Unicode support
 @section Unicode support
 @cindex symbols
@@ -2364,74 +2292,48 @@ automatically detect an appropriate one; consult the Emacs documentation
 for more details.
 
 Proof General includes two special mechanisms for assisting with input.
-The first is @b{Maths Menu} (originally by Dave Love), which simply adds
-a menu for inserting common mathematical symbols.  
+The first is @b{Maths Menu} (adapted from a menu by Dave Love), which
+simply adds a menu for inserting common mathematical symbols.
 @example
   Proof-General -> Options -> Unicode Maths Menu
 @end example
-This only works in GNU Emacs, and whether or not the symbols
-display in the menus depends on the font used to display
-the menus (which depends on the Emacs version, toolkit
+Whether or not the symbols display well the menus depends on the font
+used to display the menus (which depends on the Emacs version, toolkit
 and platform!).
 
 The second mechanism has been written specially for Proof General, to
-provide some backward compatibility with X-Symbol.  This is
+provide backward compatibility with X-Symbol.  This is
 the @b{Unicode Tokens} minor mode.
 @example
   Proof-General -> Options -> Unicode Tokens
 @end example
 The aim of this mode is to allow displaying of ASCII tokens as Unicode
-strings.@footnote{In fact, the strings are mapped to Emacs internal
-encoding for display; Unicode is just an appropriate mechanism for
-input.} This allows a file to be stored in perfectly portable plain
-ASCII encoding, but be displayed and edited with real symbols.  When the
-file is visited, the ASCII tokens are replaced by Unicode strings; when
-it is saved, the reverse happens.  For this to be reliable, you need to
-provide tokens for all the Unicode symbols you @i{don't} want to appear
-in the saved file (if any are not encoded, Emacs will try to save them
-in a richer encoding, such as UTF-8).  You also need to make sure that
-the token to symbol mapping is a bijection.
-
-The Unicode Tokens mode also provides an input mechanism for assisting
-with entering tokens, and providing short-cuts for symbols (one of the
-useful features of the X-Symbol package).  Even if your proof assistant
-manages native Unicode symbols directly, the input method and some of
-the provided commands may be useful.
-
-@kindex C-,
-@kindex C-.
-@table @kbd
-@item C-.
-@code{unicode-tokens-rotate-glyph-forward}
-@item C-,
-@code{unicode-tokens-rotate-glyph-backward}
-@item >
-@code{unicode-tokens-electric suffix}
-@end table
+character compositions, perhaps with additional text properties.
+This allows a file to be stored in perfectly portable plain
+ASCII encoding, but be displayed and edited with real symbols.  
 
+The mechanism is based on Font Lock, using the @code{composition} text
+property to display token sequences as something else.  This means that
+the underlying buffer text is not altered.  
+
+@c @kindex C-,
+@c @kindex C-.
+@c @table @kbd
+@c @item C-.
+@c @code{unicode-tokens-rotate-glyph-forward}
+@c @item C-,
+@c @code{unicode-tokens-rotate-glyph-backward}
+@c @item >
+@c @code{unicode-tokens-electric suffix}
+@c @end table
+
+
+@c DOCSTRING MAGIC: unicode-tokens-token-insert
+
+@c DOCSTRING MAGIC: unicode-tokens-rotate-glyph-forward
+
+@c DOCSTRING MAGIC: unicode-tokens-rotate-glyph-backward
 
-@c TEXI DOCSTRING MAGIC: unicode-tokens-token-insert
-@deffn Command unicode-tokens-token-insert arg &optional argname
-Insert a Unicode string by a token  name, with completion. @*
-If a prefix is given, the string will be inserted regardless
-of whether or not it has displayable glyphs; otherwise, a
-numeric character reference for whichever codepoints are not
-in the @code{unicode-tokens-glyph-list}. If argname is given, it is used for
-the prompt. If argname uniquely identifies a character, that
-character is inserted without the prompt.
-@end deffn
-@c TEXI DOCSTRING MAGIC: unicode-tokens-rotate-glyph-forward
-@deffn Command unicode-tokens-rotate-glyph-forward &optional n
-Rotate the character before point in the current code page, by @var{n} steps.@*
-If no character is found at the new codepoint, no change is made.
-This function may only work reliably for GNU Emacs >= 23.
-@end deffn
-@c TEXI DOCSTRING MAGIC: unicode-tokens-rotate-glyph-backward
-@deffn Command unicode-tokens-rotate-glyph-backward &optional n
-Rotate the character before point in the current code page, by -N steps.@*
-If no character is found at the new codepoint, no change is made.
-This function may only work reliably for GNU Emacs >= 23.
-@end deffn
 Unfortunately, the precise set of symbol glyphs that are available to
 you will depend in complicated ways on your operating system, Emacs
 version, installed font sets, and (even) command line options used to
@@ -2458,9 +2360,6 @@ an interface to the shortcuts.
 
 
 
-
-
-
 @node Imenu and Speedbar (and Function Menu)
 @section Imenu and Speedbar (and Function Menu)
 @vindex proof-goal-with-hole-regexp
@@ -2954,27 +2853,6 @@ If non-nil, display Proof General toolbar for script buffers.
 The default value is @code{t}.
 @end defopt
 
-@c TEXI DOCSTRING MAGIC: PA-x-symbol-enable
-@defopt PA-x-symbol-enable 
-Whether to use x-symbol in Proof General for this assistant.@*
-If you activate this variable, whether or not you really get x-symbol
-support depends on whether your proof assistant supports it and
-whether X-Symbol is installed in your Emacs.
-
-The default value is @code{nil}.
-@end defopt
-
-@c TEXI DOCSTRING MAGIC: proof-output-fontify-enable
-@defopt proof-output-fontify-enable 
-Whether to fontify output from the proof assistant.@*
-If non-nil, output from the proof assistant will be highlighted
-in the goals and response buffers.
-(This is providing @samp{@code{font-lock-keywords}} have been set for the
-buffer modes).
-
-The default value is @code{t}.
-@end defopt
-
 @c TEXI DOCSTRING MAGIC: proof-strict-read-only
 @defopt proof-strict-read-only 
 Whether Proof General is strict about the read-only region in buffers.@*
@@ -2994,15 +2872,6 @@ of processed text.  NB: the history manipulation only works on GNU Emacs.
 
 The default value is @code{nil}.
 @end defopt
-@c TEXI DOCSTRING MAGIC: proof-toolbar-use-button-enablers
-@defopt proof-toolbar-use-button-enablers 
-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 is @code{t}.
-@end defopt
 
 @c This one removed: proof-auto-retract
 
@@ -3047,9 +2916,9 @@ The default value is @code{nil}.
 
 @c TEXI DOCSTRING MAGIC: proof-prog-name-guess
 @defopt proof-prog-name-guess 
-If non-nil, use @samp{@code{proof-guess-command-line}} to guess @code{proof-prog-name}.@*
-This option is compatible with @code{proof-prog-name-ask}.
-No effect if @code{proof-guess-command-line} is nil.
+If non-nil, use @samp{@code{proof-guess-command-line}} to guess @samp{@code{proof-prog-name}}.@*
+This option is compatible with @samp{@code{proof-prog-name-ask}}.
+No effect if @samp{@code{proof-guess-command-line}} is nil.
 
 The default value is @code{nil}.
 @end defopt
@@ -3110,7 +2979,7 @@ If @code{'followdown}, point if necessary to stay in writeable region
 If @code{'ignore}, point is never moved after movement commands or on errors.
 
 If you choose @code{'ignore}, you can find the end of the locked using
-@samp{M-x @code{proof-goto-end-of-locked}}.
+M-x @code{proof-goto-end-of-locked}
 
 The default value is @code{locked}.
 @end defopt
@@ -3354,25 +3223,26 @@ declarations such as those above.  By default, @kbd{C-n} is
 @code{next-line} and @kbd{C-b} is @code{backward-char-command}; neither
 are really needed if you have working cursor keys.
 
-If you're using XEmacs and your keyboard has a @i{super} modifier (on my
-PC keyboard it has a Windows symbol and is next to the control key), you
-can freely bind keys on that modifier globally (since none are used
-by default).  Use lisp like this:
-@lisp
-(global-set-key [(super l)] 'x-symbol-INSERT-lambda)
-(global-set-key [(super n)] 'x-symbol-INSERT-notsign)
-(global-set-key [(super a)] 'x-symbol-INSERT-logicaland)
-(global-set-key [(super o)] 'x-symbol-INSERT-logicalor)
-(global-set-key [(super f)] 'x-symbol-INSERT-universal1)
-(global-set-key [(super t)] 'x-symbol-INSERT-existential1)
-(global-set-key [(super A)] 'x-symbol-INSERT-biglogicaland)
-(global-set-key [(super e)] 'x-symbol-INSERT-equivalence)
-(global-set-key [(super u)] 'x-symbol-INSERT-notequal)
-(global-set-key [(super m)] 'x-symbol-INSERT-arrowdblright)
-(global-set-key [(super i)] 'x-symbol-INSERT-longarrowright)
-@end lisp
-This defines a bunch of short-cuts for insert X-Symbol logical symbols
-which are often used in Isabelle.
+@c FIXME
+@c If you're using XEmacs and your keyboard has a @i{super} modifier (on my
+@c PC keyboard it has a Windows symbol and is next to the control key), you
+@c can freely bind keys on that modifier globally (since none are used
+@c by default).  Use lisp like this:
+@c @lisp
+@c (global-set-key [(super l)] 'x-symbol-INSERT-lambda)
+@c (global-set-key [(super n)] 'x-symbol-INSERT-notsign)
+@c (global-set-key [(super a)] 'x-symbol-INSERT-logicaland)
+@c (global-set-key [(super o)] 'x-symbol-INSERT-logicalor)
+@c (global-set-key [(super f)] 'x-symbol-INSERT-universal1)
+@c (global-set-key [(super t)] 'x-symbol-INSERT-existential1)
+@c (global-set-key [(super A)] 'x-symbol-INSERT-biglogicaland)
+@c (global-set-key [(super e)] 'x-symbol-INSERT-equivalence)
+@c (global-set-key [(super u)] 'x-symbol-INSERT-notequal)
+@c (global-set-key [(super m)] 'x-symbol-INSERT-arrowdblright)
+@c (global-set-key [(super i)] 'x-symbol-INSERT-longarrowright)
+@c @end lisp
+@c This defines a bunch of short-cuts for insert X-Symbol logical symbols
+@c which are often used in Isabelle.
 
 
 @node Using file variables
@@ -3963,7 +3833,7 @@ Find theorems: either of the above.
 
 The following shortcuts insert control sequences into the text,
 modifying the appearance of individual symbols (single letters,
-mathematical entities etc.); the X-Symbol package will provide immediate
+mathematical entities etc.); the Tokens package will provide immediate
 visual feedback.
 
 @table @kbd