Proof General Home

Proof General Standalone Components

As part of the Proof General project, some components have been developed which might be useful in a wider context. They are presented on this page.

As usual with free software, these programs come with no guarantees of any sort. Nonetheless, please contact us with any comments, suggestions, or problems.

Unicode Tokens Mode

This is a cut-down replacement for X-Symbol which works in recent GNU Emacs versions only. It enables a minor mode which can present sequences of characters in the buffer with alternative (typically Unicode) symbols or particular display properties (e.g., different font or sub/super script positions).

Spans: Emacs and XEmacs compatibility library for overlays/extents

Spans are an abstraction of XEmacs extents used to help bridge the gulf between GNU Emacs and XEmacs. In GNU Emacs, spans are implemented using overlays.

The library consists of three Emacs lisp files,

which implement a common interface for overlays/extents. This library was originally implemented by Healfdene Goguen. It is no longer used by Proof General, so is subject to bit rot for newer (X)Emacs versions.

See the files for further documentation, and section 12.1 of the Proof General adapting manual for more details.

Docstring magic: Elisp documentation to TeXinfo extraction

This package generates Texinfo source fragments from Emacs documentation strings which are embedded in Emacs lisp source and the running interpreter. This avoids documenting functions and variables in more than one place, and automatically adds Texinfo markup to docstrings. It's a bit like javadoc for Emacs Lisp, except that you must write a skeleton texi file which contains magic comments mentioning the function or variable names you want documented.

The package consists of one file:

which contains documentation and usage hints. For an extensive example of it's use, see the source for the PG adapting manual.

Click here to go back to the front page.

Web pages by David Aspinall. Please report issues on PG trac.
Last modified 02 February 2015.