[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

11. Configuring X-Symbol

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.

Variable: proof-xsym-activate-command

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.

Variable: proof-xsym-deactivate-command

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.

Variable: 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.