Preferences

The Toolbox's main file menu contains a Preferences item.  Clicking on it raises a dialog for setting various Toolbox preferences.  The dialog presents the following high-level choices. 

Automatic Update

General

The following items under this heading allow you to customize the Module Editor:

• The Appearance / Colors and Fonts page lets you control the font used in the Error View section of the TLC Errors View.  This can be quite useful because on some systems, the default font can appear very tiny.

• Text Editors has a Show line numbers option.  It also has an Insert spaces for tabs option that should be selected.  Several Toolbox commands do not work properly on modules containing tab characters.  A spec with tabs may not even mean what it appears to mean.  (See page 287 of Specifying Systems.)  Do not use tabs in your specs.

• The Keys page allows you to change what commands are bound to what keys.  Most of the useful ones are described here, and most of the others do nothing.  However, you may find a few useful ones that are not listed elsewhere.

Help

TLA+ Preferences

See the help page for that preference menu.  Clicking on the + next to the item reveals the following subpages.  Click on the appropriate item in the following list to see what options these preference pages provide you with.

• Module Editor Preferences
• PDF Viewer Preferences
• TLA+ Parser Preferences
• TLAPS
• TLC Model Checker Preferences