Go to the previous, next section.

Multifile Specifications

Normally, TLA+ specifications are split in several modules. There is, however, a top module whose name is by convention also the name of the whole specification. Therefore, a file `LibraryActions.t' is not the top module of the Library specification, but `Library.t' is. By using this top module as a "master file" for the rest of the modules, this relation can be used in several ways, such as issueing a command on the corresponding top module file when another module of the specification is being visited.

TLA+ mode has no inherent means to tell the name of the master file. By default, it will assume that the current file itself is a master file. If you insert the following in your `~/.emacs' file, you will be asked for the name of the top module which is the corresponding master file.

(setq-default tla-master nil)     ; query for top module

To avoid asking you again, this information will then be inserted at the very end of the module as a file variable. (See section `File Variables' in GNU Emacs Manual.)

(* Local Variables: *)
(* tla-master: "Library" *)
(* End: *)

Besides the convention that the name of the top module is also the name of the complete specification there is another convention requesting all modules belonging to the same specification to be in the same directory. Some existing tools depend on this restriction.

User Option: tla-master

The master file, i.e. the top level module, associated with the current buffer. If the file being edited is actually imported or included from another file, you can tell TLA+ mode the name of the master file by setting this variable. If there are multiple levels of nesting, specify the top level file.

If this variable is nil, TLA+ mode will query you for the name.

If the variable is t, TLA+ mode will assume the file is a master file itself.

If the variable is shared, TLA+ mode will query for the name, but will not change the file.

It is suggested that you use the File Variables (see section `File Variables' in The Emacs Editor) to set this variable permanently for each file.

Command: tla-save-specification

(C-c C-d) Save all buffers known to belong to the current specification.

Variable: tla-save-query t

If non-nil, ask user for permission when saving a buffer.

Go to the previous, next section.