Helping the Pretty-Printer

Contents
  Introduction
  How TLATeX Typesets the Specification
  How TLATeX Typesets Comments
  Using LaTeX Commands to Format Comments

Introduction

The toolbox pretty prints a module by calling the TLATeX program.  TLATeX is a Java program for typesetting TLA+ specifications with  LaTeX.  It was written by Leslie Lamport, based on ideas by Dmitri Samborski.

TLATeX's output should be good enough for most users.  Later sections describe how you can get TLATeX to do a better job, and will explain what happened in the unlikely case that it produces weird output.  However, if you happen to use any of the two-character sequences

   `~   `^   `.
 

How TLATeX Typesets the Specification

TLATeX should typeset the specification itself pretty much the way you would want it to.  It preserves most of the meaningful alignments in the specification.  For example, if the specification contains

  
  Action == /\ x'   = x - y
            /\ yy'  = 123
            /\ zzz' = zzz

then the  /\  and  =  symbols will be aligned in the output.  Extra spaces in the input will be reflected in the output.  However, TLATeX treats 0 and 1 space between symbols the same, so  x+y  and  x + y  produce the same output, but  x  +  y  produces extra space around the  + .

TLATeX typesets the single TLA+ module that must appear in the input file.  It will also typeset any material that precedes and follows the module as if it were a comment.  However, that text won't be shaded.

TLATeX does not check that the specification is syntactically correct TLA+ input.  However, it will report an error, which will be reported to you by the Toolbox, if the specification contains an illegal lexeme, such as a semicolon (;).

How TLATeX Typesets Comments

                                                               
    `~   `^   `.                                                 

TLATeX distinguishes between one-line and multi-line comments.  A one-line comment is any comment that is not a multi-line comment.  Multi-line comments can be typed in any of the following three ways:

  (*************************)
  (* This is the text of a *)
  (* multi-line comment.   *)
  (*************************)

  \********************
  \* This is the text 
  \* of the comment.  
  \********************

  (* This is the text
     of the comment.   *)

In the first two ways, the  (*  or  \*  characters on the left must all be aligned, and the last line of  *  characters is optional.  In the first way, nothing may appear to the right of the comment--otherwise, the input is considered to be a sequence of separate one-line comments.  In a multi-line comment, TLATeX usually considers a sequence of non-blank lines to be a single paragraph, in which case it will typeset them as one paragraph and ignore the line breaks in the input.

TLATeX does its best to do a sensible job of typesetting comments.  You can help it by ending each sentence with a period (.) and by adding blank lines to indicate logical separation of items.

There are three ways in which TLATeX can mess up the typesetting of comments:

1. Parts of a specification, such as identifiers and certain operators like  - , should be typeset differently from ordinary text.  Identifiers should be italicized, and the minus in the expression  x-y  should be typeset differently from the dash in  x-ray.  TLATeX gets this right most of the time, but it does make mistakes.

   You can tell TLATeX to treat something as part of a specification by putting single quotes  (`  and  ')  around it.  You can tell TLATeX to treat something as ordinary text by putting  `^  and  ^'  around it--for example:

          \***********************************
          \* To find the latest value of `bar',
          \* see `^http::/frob/bar^'.
          \***********************************
   

   But, this is seldom necessary.  TLATeX usually does the right thing.

   WARNING: Do not put any character between  `^  and  ^'  except letters, numbers, and ordinary punctuation.  In particular, do not put any of the following characters between  `^  and  ^':

                                                              
           _  ~  #  $  %  ^  &  <  >  \ "                     
   

   See the section below on using LaTeX commands in comments for further information about what can go between  `^  and  ^'.
2. TLATeX does not do any fancy formatting of paragraphs.  For example, TLATeX will not precisely align the "A"s when typesetting:

          \***********************
          \* gnat: A tiny insect.
          \*
          \* gnu:  A short word.
          \***********************
   

   You can tell TLATeX to typeset a sequence of lines precisely the way they appear in the input, using a fixed-width font, by enclosing the lines with `. and .' , as in:

          \**********************************************
          \* The following picture explains everything:
          \*
          \*      `. -----------          --------
          \*        | Processor |------->| Memory |   
          \*         -----------          --------  .'
          \**********************************************
   

   Using  `.  and  .'  is the only reasonable thing to do for a diagram.  However, if you know (or want to learn) LaTeX, the section below on using LaTeX commands in comments will explain how you can get TLATeX to do a good job of formatting things like lists and tables.
3. A paragraph may be typeset loosely, with one or more lines containing    lots    of    space    between    the    words.  This happens if there is no good way to typeset the paragraph.  If this bothers you, the easiest solution is to rewrite the paragraph.  You can also try to fix the problem with LaTeX commands.  (See the section below on using LaTeX commands to format comments.)

TLATeX ignores any  (*  ...  *)  comment that appears within another comment.  So, you can get it not to typeset part of a comment by enclosing that part between  (*  and  *)  But a better way to omit part of a comment is to enclose it between  `~  and  ~'.

Using LaTeX Commands to Format Comments

1. You can enclose between `^ and ^' a short phrase appearing on a single line of input.  LaTeX typesets that phrase as part of the enclosing paragraph.
2. You can enclose one or more complete lines of a multi-line comment between  `^  and  ^' .  That text is typeset as one or more separate paragraphs whose prevailing left margin is determined by the position of the   `^ .  For example, the input

          \**********************************
          \* The first comment paragraph.
          \*
          \*    The second comment
          \*    paragraph.
          \*
          \*    `^ Some LaTeX-formated 
          \*  text  ^'
          \**********************************
   

   causes the LaTeX-formated text to be typeset in a separate paragraph whose prevailing left margin is the same as in the second comment paragraph.

       \***********************
       \*    `^ \begin{describe}{gnat:}
       \*        \item[gnat:] A tiny insect.
       \*  
       \*        \item[gnu:]  A short word.
       \*       \end{describe} ^'
       \***********************

Warning: An error in a LaTeX command inside   `^ ... ^'  text can cause TLATeX not to produce any output.

TLATeX has a feature that is not relevant to use with the Toolbox that involves putting code between  `~  and  ~' .  Unless you are also using TLATeX outside the Toolbox and know what you're doing, do not put   `~  or  ~'  in comments.