Pretty-Printing Modules

You can create and view a pretty-printed PDF (Portable Document Format) version of a module. Just view the module in a module editor and select File/Produce PDF Version. However, to do this, you must have the pdflatex program installed. This program is distributed with most versions of LaTeX and TeX. A popular source of TeX for PCs is MiKTeX.

The Toolbox runs pdflatex to produce a PDF file with the same name as the module, but with the extension .pdf. It displays this file in a separate page of the module editor, using your computer's default browser to display the PDF file. (If the browser doesn't have a plug-in that displays PDF files, you can find one on the web.) You can switch between the editable ASCII version of the module and the PDF version by clicking on the appropriate tab in the lower-left corner. Changes made to the module are not automatically made to the PDF version. To see them, you must create the PDF version again.

There are things you can do to help the pretty printer produce better output. They are described in the Helping the Pretty-Printer help page.

A version of the program that does the pretty-printing can be used to add TLA+ and/or PlusCal code to a LaTeX document. See the section on the TLATeX Pretty-Printer on this page of the TLA+ Web site.

Preferences

The PDF Viewer Preferences page on the File/Preferences menu provides the following options:

'Have your OS open PDFs' (macOS) or 'Use built-in PDF viewer' (Windows & Linux)

By default, the PDF file is displayed using your system's default PDF viewer. This option causes the Toolbox to instead either have the operating system open the PDF using the user's default PDF viewing application (in macOS) or to use its own built-in viewer (in Windows and Linux.) On some systems, the default viewer displays the PDF file in a separate window that you must close before you can generate a new version of the file. If that is not what you want to happen, choose this option. The built-in viewer does not yet provide a toolbar. You can navigate with the Page Up and Page Down keys. Use the + and - keys to zoom in and out. The built-in viewer option is not offered on Mac OS X.

Regenerate pretty-printed PDF of spec save

When checked, the Toolbox automatically updates the pretty-printed version of the module every time its corresponding editor is saved. This is especially useful in presentations and trainings when the spec editor and PDF viewer are arranged side by side to interactively build-up the spec but show attendees the pretty-printed version.

Shade comments

Comments are shaded in gray. This is the default. The darkness of the shading is specified by the Specify gray level option. This must be a number between 0.0 (completely black) and 1.0 (no shading). The default is 0.85.

Note that comments within comments are not shown in the PDF view. The one exception is that comments to PlusCal code are shown (even though they and the PlusCal code appear in a comment).

Do not shade PlusCal code

A PlusCal algorithm appears in a comment, so shading comments normally causes PlusCal code to be shaded. This option causes PlusCal code not to be shaded. (The code's comments are still shaded.)

Number lines

Number lines in the PDF output. (This is independent of the line-numbering option for the module editor.) The default is unnumbered lines.

Specify dot command

This is the command with which the Toolbox calls dot to produce state graph visualizations. The default value dot should work if the dot program is installed on your computer. However, if it is not properly installed, you may have to prefix it with the path name of the program's directory.

Specify pdflatex command

This is the command with which the Toolbox calls pdflatex to produce the pretty-printed version. The default value pdflatex should work if the pdflatex program is installed on your computer. However, if it is not properly installed, you may have to prefix it with the path name of the program's directory.

Specify gray level

See the Shade comments option above.

Subtopics: Helping the Pretty-Printer

↑ Managing Your Specifications