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

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 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).


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

This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.