Merge changes from Version4Branch.

1 files changed, 89 insertions, 128 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.