Go to the previous, next section.

Introduction

This is a major mode for GNU Emacs (and derivatives) that serves as an environment for the specification process in TLA+, a specification language proposed by Leslie Lamport.

Apart from supporting the process of editing and modifying specifications by means of indentation and template insertion it also integrates related applications and tools via a common interface. It works not only with single files but with a whole range of files that syntactically constitute a TLA+ specification.

Together with a preliminary support for different variants of TLA+ this mode is designed to serve all users that are involved in writing specification code.

Here is a list of the major features:

• Insertion of templates such as module headers and keywords
• Short cuts for easy access to syntactic elements
• Sophisticated indentation for most tTLA+ expressions
• Support for multi-module specifications
• Running programs such as TeX, tpp or TBR
• Parsing tpp error messages
• Outlining for specifications
• Fontified specifications

Go to the previous, next section.