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, and the User Output and Progress Output sections of the Model Check Results.   This can be quite useful because on some systems, the default font can appear very tiny.
• The Appearance / Colors and Fonts page lets you also control the font used in the Error-Trace viewer section of the TLC Errors View.
• The Editors / 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.
• The News page lets you choose whether you want the Toolbox to inform you about news from TLA+ RSS feeds; there are two feeds enabled by default.

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.

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