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 include
|5.1 Syntax highlighting|
|5.2 Imenu and Speedbar|
|5.3 Support for outline mode|
|5.4 Support for completion|
|5.5 Support for tags|
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
To automatically switch on fontification in Emacs, you may need
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.
5.2 Imenu and Speedbar
The Emacs package
imenu (Index Menu) provides 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-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 -> Quick Options -> Minor Modes -> 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.
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
Proof-General -> Quick Options -> Minor Modes -> Speedbar
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.
5.3 Support for outline mode
Proof General configures Emacs variables (
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
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 (emacs)Outline Mode for more information about outline mode.
5.4 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
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.
PA-completion-table holds the list of
identifiers for a proof assistant. The function
proof-add-completions adds these into the completion
- Variable: PA-completion-table
List of identifiers to use for completion for this proof assistant.
Completion is activated with M-x complete.
If this table is empty or needs adjusting, please make changes using ‘
customize-variable’ and post suggestions at https://github.com/ProofGeneral/PG/issues
The completion facility uses a library ‘completion.el’ which
usually ships with Emacs, and supplies the
- Command: complete
Fill out a completion of the word before point.
Point is left at end. Consecutive calls rotate through all possibilities. Prefix args:
leave point at the beginning of the completion, not the end.
- a number
rotate through the possible completions by that amount
same as -1 (insert previous completion)
See the comments at the top of ‘completion.el’ for more info.
5.5 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,
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.
This document was generated by Erik Martin-Dorel on August 21, 2021 using texi2html 1.82.