Go to the previous, next section.

Running Commands

Since there are a number of tools involved in the specification process, being able to run them is essential for the quality of the TLA+ working environment.

The commands that are available at your site depend on the configuration of tla-command-list. These are the standard commands:

Name

Command

Browse

Launch "tTLA+Browser" with the name of the current top module or buffer as argument.

Check

Run tpp, the preprocessor of the "tTLA+Browser", with the name of the current top module or buffer as argument.

LaTeX

Run LaTeX in nonstop mode together with the `spec92.sty' style file on the current buffer.

User Option: tla-command-list

List of commands to execute on the current module or specification.

Each element is a list, whose first element is the name of the command as it will be presented to the user. The second element is the string handed to the shell after being expanded. The expansion accounts for different types of files. The third element is the function which actually start the process. Several such hooks has been defined which are explained in more detail in the source code.

Executing Commands

Analyzing the specification with the help of tpp, launching applications such as TBR, or documenting the current module by using Lamport's `spec92.sty' all require running an external command. Currently, you can only issue commands involving the whole specification with tla-command-master.

Command: tla-command-master

(C-c C-c) Query the user for a command, and run it on the master file (top level module) associated with the current buffer. The name of the master file is controlled by the variable tla-master. The available commands are controlled by the variable tla-command-list.

Command: tla-command-buffer

(C-c C-b) Query the user for a command, and run it on the current buffer. The available commands are controlled by the variable tla-command-list.

User Option: tla-command-default nil

The default command to run in this buffer. Must be an entry in tla-command-list.

Controlling Output

The following commands allow the user to control the output of a command. They are also accessible via the "Command Output" menu.

Command: tla-kill-job

(C-c C-k) Kill external command currently running. This may be either a command of tpp, TBR, TeX etc.

Command: tla-recenter-output-buffer

(C-c C-l) Recenter the output buffer so that the bottom line is visible.

Command: tla-home-buffer

(C-c ^) Go to the top module of the specification associated with the current buffer, or if already there, to the file where the current process was started.

When `debugging" specifications with the help of tpp, you may browse through the errors. While it is possible to offer such support for other tools as well, this has been realized so far only for tpp.

Command: tla-next-error

(C-c `) Go to the next error reported by tpp (invoked by "Check"). The view will be split into two, with the cursor placed as close as possible to the error in the top view.

Go to the previous, next section.