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.
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 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,
See the files for further documentation, and section 12.1 of the Proof General adapting manual for more details.
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.