Editing Modules

Contents
  Module Editors
  Finding Definitions and Declarations and Their Uses
  Finding PlusCal Source Code
  Editing Comments
  Editing and Viewing Proofs
  Miscellaneous Commands
  Module Editor Key Bindings

Module Editors

When you first open a spec, the Toolbox shows the root module in a module editor view.  You can open additional modules in separate module editor views by clicking  File/Open Module.  This will allow you to select a module, either from a list of modules that are or were part of the spec or from a file browser.  You can also create a new module file in the file browser.  You can select a module only from the same folder as the root-module file.

If you have multiple module editors open, you can switch between them by clicking on the editor's tab.  A  *  in the tab means that there are unsaved changes to the module.  Clicking on the  X  at the right of the tab deletes the module editor (but not the module).  If you accidentally delete a module editor, you can re-open the module as described above.

It's sometimes useful to open two views on the same module, so you can view different parts of it at the same time.  You can do this by right-clicking on the module editor's tab and selecting  New Editor.  See the Managing Views help page for how to put model editors where you want them in the Toolbox window.  See the Pretty-Printing Modules help page for how to view the pretty-printed versions of your modules.

A module editor provides the usual text editing commands for editing the module.  There are  Save  and  Save As  commands on the   File  menu.  (Typing  Control+s  also performs the save command.)  The  Edit  menu provides a few familiar commands.  Below is a list of available commands and the keys to which they are bound. 

If you create a new module file with the Toolbox, the module editor will create a modification history at the end of the file that begins with the line

   \* Modification History   

If you want to prevent the Toolbox from adding the modification history comment, you can disable this in the TLA+ Preferences/Model Viewer section of the Preference menu.

The Toolbox maintains a history of previous versions of a module.  It adds the current version to the history every time you save the module.  You can examine and revert to a version from the history by right-clicking on in the module editor and selecting Team, Compare With, or Replace With.  You can also right-click on any module of the open specification in the Spec Explorer and select Show in History.

Finding Definitions, Declarations, and Their Uses

The module editor provides commands for finding the PlusCal code that finding the definition or declaration of a user-defined symbol, for finding all uses of that definition or declaration, and for finding all symbols defined and declared in the module.  For brevity, the names of all of these commands use the term declaration instead of declaration or definition. These commands can be executed by right-clicking on the editor and selecting the command from the popped-up menu, or with the keystroke indicated on the menu.  The General/Keys item on the Preference menu allows you to change those key bindings.  The Goto Declaration command can also be executed by control + click, as explained below.

For the commands that find the declaration or uses of a symbol, the symbol is the one containing the cursor (caret) or that the cursor is right before.  It is not the one being pointed at by the mouse--except when using the control + click version of the Goto Declaration command.

Most of these commands work only if the spec is successfully parsed--that is, if its status (indicated at the bottom of the window) is parsed (green).  If the module has been modified since the spec was parsed, a command may not work properly. The Goto Declaration command may not recognize the symbol, and a command that should highlight and/or jump to someplace in the module may highlight or jump to the wrong place.  However, if the Show Uses command is executed before the module is modified, then the highlighting and subsequent Goto Prev/Next Use commands will work properly.

Goto Declaration (F3)

This command jumps to the definition or declaration of the chosen symbol, which must not be a built-in TLA+ symbol or a symbol defined in a standard module.  This could mean jumping to a different module.  In addition to executing the command from a menu or by typing F3, you can also hold down the Control key and move the mouse over the symbol.  When the mouse is over a declared or user-defined symbol, the symbol will change appearance and turn into a link that you can left-click on to jump to the symbol's declaration or definition.

Return From Goto (F4)

Show Declarations (F5)

This command raises a menu containing a list of all the symbols defined and declared in the current module.  You can jump to a symbol's definition or declaration by selecting that symbol from the list.  You can select an item from the list by clicking on it, or by selecting the desired item--with a combination of the arrow keys and typing the first few letters of its name--and then typing Enter. 

Typing space causes the menu to toggle between showing and hiding definitions that are imported by instantiation.  (More precisely, it applies to definitions that are imported with renaming and/or with substitution for module parameters.)

Show Uses (F6)

This command highlights all uses of the selected symbol and enables the Goto Next Use and Goto Prev Use commands.  If the symbol is used in more than one module, it raises a menu allowing you to select the desired module from a list.  You can select a module from the list by clicking on it, or by selecting it--with a combination of the arrow keys and typing the first few letters of its name--and then typing Enter.

The highlighting of the uses is cleared by executing another Show Uses command or by re-parsing the specification.  Whether or not re-parsing the specification clears the highlighting is controlled by an editor preference.

Goto Prev/Next Use (F7/F8)

Finding PlusCal Source Code

After you have successfully run the PlusCal translator to translate an algorithm, the Goto PCal Source command (F10) allows you to jump from a selected region of the TLA+ translation to the PlusCal code that generated it.  Select a region of the TLA+ specification, and the command jumps to and highlights approximately the smallest syntactic unit of the PlusCal algorithm whose translation contains the selected region.  (You can select a single token by putting the cursor in or next to it.)  The command does nothing if that smallest syntactic unit is the entire algorithm, or if the selected region does not lie within the algorithm's translation. The Return From Goto command (F4) jumps back to the original selection. 

Clicking on parsing error reports, and on error reports and some other fields in a TLC model window, highlights and jumps to a region of the TLA+ spec.  If that region of the spec was produced by the PlusCal translation, the Goto PCal Source command should then take you to the appropriate part of the PlusCal source code.  You can also jump directly to the PlusCal source by control-clicking (holding the CONTROL key while clicking) on the error report.  That will take you to the region of the TLA+ spec if it has no corresponding PlusCal region.

The mapping from regions of the TLA+ translation to regions of the PlusCal source is determined at the time of translation.  If the PlusCal source, the translation, or any part of the module lying between them is changed, then the command may jump to the wrong place.  It's best to put the translation immediately after the comment containing the algorithm.  If you omit the BEGIN/END TRANSLATION comments, that is where the translation will be put.

Editing Comments

The TLA+ Pretty Printer regards a comment "boxed" as follows to be a sequence of paragraphs.

  (**************************************)
  (* This is the                        *)
  (*   first paragraph.                 *)
  (*                                    *)
  (*   This text is a display           *)
  (*                                    *)
  (* This is another paragraph.         *)
  (**************************************)

The module editor provides the commands for creating and editing boxed comments.  They make boxed comments that extend from some specified point to a right margin--a column specified by a preference..  These commands are executed by typing two characters, the first of which is Ctl+O.  If you type Ctl+O and wait a moment, the list of all these commands will appear.  The commands can also be executed by right-clicking on the mouse.  For these commands, the current position is the location where the typing cursor is, not where the mouse is pointing. 

To create a comment, you first position cursor where you want the top left-hand corner of the comment and execute the Start Boxed Comment by typing Ctl+O Ctl+S.  This produces the comment begin and end tokens like this:

Beauty == TRUE  (***********************************

                ***********************************)

Beauty == TRUE  (***********************************
This is 
a
very interesting formula, 
because it expresses Keats' famous dictum

  Beauty is truth
  and truth beauty.
         
How much more than this do you really need to know?
               ***********************************)

Beauty == TRUE  (***********************************
This is a very interesting 
formula, because it expresses
Keats' famous dictum

  Beauty is truth
  and truth beauty.
         
How much more than this do you 
really need to know?
               ***********************************)

Beauty == TRUE  (**********************************)
                (* This is a very interesting     *)
                (* formula, because it expresses  *)
                (* Keats' famous dictum           *)
                (*                                *)
                (*   Beauty is truth              *)
                (*   and truth beauty.            *)
                (*                                *)
                (* How much more than this do you *)
                (* really need to know?           *)
                (**********************************)

To modify an existing boxed comment, put the cursor inside the comment box and execute the Unbox Comment command by typing Ctl+O Ctl+U.  You can then edit and rebox it with the commands described above.

Editing and Viewing Proofs

Miscellaneous Commands

Goto Matching Parenthesis (Control+Shift+p)

     (  )    [  ]    {  }    <<  >>    (*  *)

Toggle Block Selection Mode (Alt+Shift+a)

The module is displayed in Text Editor Block Selection Font instead of Text Font when in Block Selection Mode.  You can change those fonts by selecting General / Appearance / Colors and Fonts on the Preference menu.

Module Editor Key Bindings