11. Configuring Tokens
Unicode Tokens is basically an overly complicated way of configuring
font-lock, along with some helpful menus. The font lock configuration
makes use of recent Emacs features, particularly including
compose-region which allows the presentation of the buffer be
different from the underlying buffer contents. Compared with the
X-Symbol package used previously by Proof General, this has the huge
advantage of not requiring the underlying text to be changed to display
symbols.
Usage of the Unicode Tokens package is described in the Proof General user manual, see (ProofGeneral)Unicode symbols and special layout support.
- Variable: proof-tokens-activate-command
Command to activate token input/output for prover.
If non-nil, this command is sent to the proof assistant when Unicode Tokens support is activated.
- Variable: proof-tokens-deactivate-command
Command to deactivate token input/output for prover.
If non-nil, this command is sent to the proof assistant when Unicode Tokens 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 Tokens
to display special characters in the same token language. This happens
automatically. If you want additional modes to use Tokens with the
token language for your proof assistant, you can set
proof-tokens-extra-modes.
- Variable: 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).
This document was generated on April 18, 2024 using texi2html 1.82.