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.

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,

• span-extent.el
• span-overlay.el
• span.el (which simply loads one of the above)

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:

• texi-docstring-magic.el