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

# 5. Support for other Packages

Proof General makes some configuration for other Emacs packages which provide various useful facilities that can make your editing more effective.

Sometimes this configuration is purely at the proof assistant specific level (and so not necessarily available), and sometimes it is made using Proof General settings.

When adding support for a new proof assistant, we suggest that these other packages are supported, as a convention.

The packages currently supported are `font-lock`, `x-symbol`, `func-menu`, `outline-mode`, `completion`, and `etags`.

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

## 5.1 Syntax highlighting

Proof script buffers are decorated (or fontified) with colours, bold and italic fonts, etc, according to the syntax of the proof language and the settings for `font-lock-keywords` made by the proof assistant specific portion of Proof General. Moreover, Proof General usually decorates the output from the proof assistant, also using `font-lock`.

In XEmacs, fontification is automatically turned on. To automatically switch on fontification in GNU Emacs 20.4, you may need to engage `M-x global-font-lock-mode`. The old mechanism of adding hooks to the mode hooks (`lego-mode-hooks`, `coq-mode-hooks`, etc) is no longer recommended; it should not be needed in latest Emacs versions which have more flexible customization.

Fontification for output is controlled by a separate switch in Proof General. Set `proof-output-fontify-enable` to `nil` if you don't want the output from your proof assistant to be fontified according to the setting of `font-lock-keywords` in the proof assistant specific portion of Proof General. See section User options.

By the way, the choice of colour, font, etc, for each kind of markup is fully customizable in Proof General. Each face (Emacs terminology) is controlled by its own customization setting. You can display a list of all of them using the customize menu:

    Proof General -> Advanced -> Customize -> Faces -> Proof Faces.

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

## 5.2 X-Symbol support

The X-Symbol package displays characters from a variety of fonts in Emacs buffers, automatically converting between codes for special characters and tokens which are character sequences stored in files.

Proof General uses X-Symbol to allow interaction between the user and the proof assistant to use tokens, yet appear to be using special characters. So proof scripts and proofs can be processed with real mathematical symbols, Greek letters, etc.

The X-Symbol package is now bundled with Proof General. You will be able to enable X-Symbol support if support has been provided in Proof General for a token language for your proof assistant. To enable X-Symbol, use the menu item:

      Proof-General -> Options -> X-Symbol

To enable it automatically every time you use Proof General, just use

      Proof-General -> Options -> Save Options

once it has been selected. (Alternatively, customize the setting `PA-x-symbol-enable`).

You may also simply use `M-x x-symbol-mode` to turn on and off X-Symbol display in the scripting buffer, as you would when using X-Symbol for other modes, or indeed, as for any other Emacs minor mode. However, this way of turning on and off symbols will only affect the current script buffer, and will not change the status of any symbol configuration for the prover input/output (some proof assistants, such as Isabelle, have switches for enabling symbol output). To make sure that symbol output is switched on or off for the prover as a whole, use the menu option mentioned above, or its underlying command, `M-x proof-x-symbol-toggle`.

Notice that for proper symbol support, the proof assistant needs to have a special token language, or a special character set, to use symbols. In this case, the proof assistant will output, and accept as input, tokens like `\longrightarrow`, which display as the corresponding symbols. However, for proof assistants which do not have such token support, we can use "fake" symbol support quite effectively, displaying ordinary ASCII character sequences such as `-->` with symbols.

For more information about the X-Symbol package, please visit its home page at http://x-symbol.sourceforge.net/.

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

## 5.3 Unicode support

Proof General inherits support for displaying Unicode (and any other) fonts from the underlying Emacs program. If you are lucky, your system will be able to use (or synthesise) a font that provides a rich set of mathematical symbols. To store these symbols in files you need to use a particular coding, for example UTF-8. In fact, Modern Emacsen can handle a multitude of different coding systems and will try to automatically detect an appropriate one; consult the Emacs documentation for more details.

Proof General includes two special mechanisms for assisting with input. The first is Maths Menu (originally by Dave Love), which simply adds a menu for inserting common mathematical symbols.

      Proof-General -> Options -> Unicode Maths Menu

This only works in GNU Emacs, and whether or not the symbols display in the menus depends on the font used to display the menus (which depends on the Emacs version, toolkit and platform!).

The second mechanism has been written specially for Proof General, to provide some backward compatibility with X-Symbol. This is the Unicode Tokens minor mode.

      Proof-General -> Options -> Unicode Tokens

The aim of this mode is to allow displaying of ASCII tokens as Unicode strings.(7) This allows a file to be stored in perfectly portable plain ASCII encoding, but be displayed and edited with real symbols. When the file is visited, the ASCII tokens are replaced by Unicode strings; when it is saved, the reverse happens. For this to be reliable, you need to provide tokens for all the Unicode symbols you don't want to appear in the saved file (if any are not encoded, Emacs will try to save them in a richer encoding, such as UTF-8). You also need to make sure that the token to symbol mapping is a bijection.

The Unicode Tokens mode also provides an input mechanism for assisting with entering tokens, and providing short-cuts for symbols (one of the useful features of the X-Symbol package). Even if your proof assistant manages native Unicode symbols directly, the input method and some of the provided commands may be useful.

`C-.`

  `unicode-tokens-rotate-glyph-forward`

`C-,`

  `unicode-tokens-rotate-glyph-backward`

`>`

  `unicode-tokens-electric suffix`

Command: unicode-tokens-token-insert arg &optional argname

  Insert a Unicode string by a token name, with completion.
  If a prefix is given, the string will be inserted regardless of whether or not it has displayable glyphs; otherwise, a numeric character reference for whichever codepoints are not in the `unicode-tokens-glyph-list`. If argname is given, it is used for the prompt. If argname uniquely identifies a character, that character is inserted without the prompt.

Command: unicode-tokens-rotate-glyph-forward &optional n

  Rotate the character before point in the current code page, by n steps.
  If no character is found at the new codepoint, no change is made. This function may only work reliably for GNU Emacs >= 23.

Command: unicode-tokens-rotate-glyph-backward &optional n

  Rotate the character before point in the current code page, by -N steps.
  If no character is found at the new codepoint, no change is made. This function may only work reliably for GNU Emacs >= 23.

Unfortunately, the precise set of symbol glyphs that are available to you will depend in complicated ways on your operating system, Emacs version, installed font sets, and (even) command line options used to start Emacs. Describing the full range of possibilities or giving recommendations is beyond the scope of this manual; please search (and contribute!) to the Proof General wiki at http://proofgeneral.inf.ed.ac.uk/wiki for more details.

To edit the strings used to display tokens, or the collection of short-cuts, you can edit the file `PA-unicode-tokens.el`, or customize the two main variables it contains: `PA-token-name-alist` and `PA-shortcut-alist`. E.g., for Isabelle

      M-x customize-variable isar-token-name-alist RET

provides an interface to the tokens, and

      M-x customize-variable isar-shortcut-alist

an interface to the shortcuts.

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

## 5.4 Imenu and Speedbar (and Function Menu)

The Emacs packages `imenu` (Index Menu) and `func-menu` (Function Menu) each provide a menu built from the names of entities (e.g., theorems, definitions, etc) declared in a buffer. This allows easy navigation within the file. Proof General configures both packages automatically so that you can quickly jump to particular proofs in a script buffer.

(Developers note: the automatic configuration is done with the settings `proof-goal-with-hole-regexp` and `proof-save-with-hole-regexp`. Better configuration may be made manually with several other settings, see the Adapting Proof General manual for further details).

To use Imenu, select the option

            Proof General -> Options -> Index Menu

This adds an "Index" menu to the main menu bar for proof script buffers. You can also use `M-x imenu` for keyboard-driven completion of tags built from names in the buffer.

To use Function Menu (distributed only with XEmacs), use `M-x function-menu`. To enable it by default each time you visit a proof script file (i.e. avoid typing `M-x function-menu`), you should find the file ‘`func-menu.el`’ and follow the instructions there.

Speedbar displays a file tree in a separate window on the display, allowing quick navigation. Middle/double-clicking or pressing `+` on a file icon opens up to display tags (definitions, theorems, etc) within the file. Middle/double-clicking on a file or tag jumps to that file or tag.

To use Speedbar, use

            Tools -> Display Speedbar

(for GNU Emacs), or

            Proof General -> Advanced -> Speedbar

(for XEmacs). If you prefer the old fashioned way, `M-x speedbar' does the same job.

For more information about Speedbar, see http://cedet.sourceforge.net/speedbar.shtml.

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

## 5.5 Support for outline mode

Proof General configures Emacs variables (`outline-regexp` and `outline-heading-end-regexp`) so that outline minor mode can be used on proof script files. The headings taken for outlining are the "goal" statements at the start of goal-save sequences, see section Goal-save sequences. If you want to use `outline` to hide parts of the proof script in the locked region, you need to disable `proof-strict-read-only`.

Use `M-x outline-minor-mode` to turn on outline minor mode. Functions for navigating, hiding, and revealing the proof script are available in menus.

Please note that outline-mode may not work well in processed proof script files, because of read-only restrictions of the protected region. This is an inherent problem with outline because it works by modifying the buffer. If you want to use outline with processed scripts, you can turn off the `Strict Read Only` option.

See See ((xemacs))Outline Mode for more information about outline mode.

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

## 5.6 Support for completion

You might find the completion facility of Emacs useful when you're using Proof General. The key `C-RET` is defined to invoke the `complete` command. Pressing `C-RET` cycles through completions displaying hints in the minibuffer.

Completions are filled in according to what has been recently typed, from a database of symbols. The database is automatically saved at the end of a session.

Proof General has the additional facility for setting a completion table for each supported proof assistant, which gets loaded into the completion database automatically. Ideally the completion table would be set from the running process according to the identifiers available are within the particular context of a script file. But until this is available, this table may be set to contain a number of standard identifiers available for your proof assistant.

The setting `PA-completion-table` holds the list of identifiers for a proof assistant. The function `proof-add-completions` adds these into the completion database.

Variable: PA-completion-table

  List of identifiers to use for completion for this proof assistant.
  Completion is activated with c-ret.

  If this table is empty or needs adjusting, please make changes using ‘``customize-variable``’ and post suggestions at http://proofgeneral.inf.ed.ac.uk/trac

The completion facility uses a library ‘`completion.el`’ which usually ships with XEmacs and GNU Emacs, and supplies the `complete` function.

Command: complete

  Fill out a completion of the word before point.
  Point is left at end. Consecutive calls rotate through all possibilities. Prefix args:

  `C-u`

    leave point at the beginning of the completion, not the end.

  `a number`

    rotate through the possible completions by that amount

  `0`

    same as -1 (insert previous completion)

  See the comments at the top of ‘`completion.el`’ for more info.

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

## 5.7 Support for tags

An Emacs "tags table" is a description of how a multi-file system is broken up into files. It lists the names of the component files and the names and positions of the functions (or other named subunits) in each file. Grouping the related files makes it possible to search or replace through all the files with one command. Recording the function names and positions makes possible the `M-.` command which finds the definition of a function by looking up which of the files it is in.

Some instantiations of Proof General (currently LEGO and Coq) are supplied with external programs (‘`legotags`’ and ‘`coqtags`’) for making tags tables. For example, invoking ‘`coqtags *.v`’ produces a file ‘`TAGS`’ for all files ‘`*.v`’ in the current directory. Invoking ‘`coqtags `find . -name \*.v``’ produces a file ‘`TAGS`’ for all files ending in ‘`.v`’ in the current directory structure. Once a tag table has been made for your proof developments, you can use the Emacs tags mechanisms to find tags, and complete symbols from tags table.

One useful key-binding you might want to make is to set the usual tags completion key `M-tab` to run `tag-complete-symbol` to use completion from names in the tag table. To set this binding in Proof General script buffers, put this code in your ‘`.emacs`’ file:

    (add-hook 'proof-mode-hook
      (lambda () (local-set-key '(meta tab) 'tag-complete-symbol)))

Since this key-binding interferes with a default binding that users may already have customized (or may be taken by the window manager), Proof General doesn't do this automatically.

Apart from completion, there are several other operations on tags. One common one is replacing identifiers across all files using `tags-query-replace`. For more information on how to use tags, See ((xemacs))Tags.

To use tags for completion at the same time as the completion mechanism mentioned already, you can use the command `M-x add-completions-from-tags-table`.

Command: add-completions-from-tags-table

  Add completions from the current tags table.

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

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.