TEM - a TLA+ Mode for EMACS

Computer Networks and Distributed Systems Group (RvS)

University of Dortmund, CS Dept.

A new alpha release (0.4) of TLA+ Mode has been released. This is a major mode for GNU Emacs 19 for supporting the specification process of TLA-based specification languages.

Features

parsing error messages from TPP (tTLA+Browser)
support for running commands on the top module of the current specification or on the current buffer
generating LaTeX files conforming to spec92.sty
support for handling multifile specifications
support for font-locking
easy accessible insertion of headers and keyword templates via menu or keyboard shortcut
sophisticated indentation for a wide range of tTLA+ expressions
supporting nested bulleted lists of conjunctions and disjunctions
partial semantic analysis with error handling
flexible commenting of lines, regions and symbol definitions
outlining of specifications
direct menu access to on-line documentation
easy bug-reporting thanks to the reporter package from Barry Warsaw

Problems

not in all functions compatible to Lucid Emacs
support for Emacs 18 dropped
no thorough support for file extensions other than default ".t"

Please use the bug reporter to send comments and bugs to

tla-mode-bugs@linguistics.ruhr-uni-bochum.de

Distribution

This is the complete release: tla-mode-0.4.tar.gz. If you don't want to bother about generating the documentation, consider taking the complete documentation in DVI, Info, PostScript and HTML, which may also be read online ( html, Postscript, Reference Card in Postscript) .

This is definitely the last alpha release. See the file NEWS in the distribution for a list of user-visible changes. See the file TODO for a list of current bugs.

Author

Frank Wegmann wrote software, documentation and Web-pages as part of his diploma thesis (completed Oct 94) in the Tools for TLA-based specifications project.

As maintainer he also keeps his software available on his own FTP archive.

Arnulf Mester, 18 Nov 1994

Informatik IV, Uni Dortmund