Go to the previous, next section.
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
Browse
Check
LaTeX
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.
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
.
(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
.
(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
.
The following commands allow the user to control the output of a command. They are also accessible via the "Command Output" menu.
(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.
(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.
(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.