[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 of how X-Symbol works: read the documentation that is supplied with it.
The basic task is to set up a token language for your proof
assistant. If your assistant is stored in the subdirectory
myprover, the token language will be called myprover and be
defined in a file `x-symbol-myprover.el' which is
automatically loaded by X-Symbol. The name of the token language mode
will be myproversym
.
Proof General will check that the file `x-symbol-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 `myprover.el'. These settings are optional.
Command to activate token input/output for X-Symbol.
If non-nil, this command is sent to the proof assistant when
X-Symbol support is activated.
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 deactivated.
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
to display special characters in the same token language. This happens
automatically. If you want additional modes to use X-Symbol with the
token language for your proof assistant, you can set
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,
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).
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.