Editing Modules

  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   
You can move the modification history anywhere you want in the file.  If you created the file outside the Toolbox, you can put this history-beginning line anywhere you want.  However, the line must appear exactly as shown, with no spaces before the  \*  and exactly one space after it.

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)

This command jumps back to the location from which the most recent Goto Declaration or Goto PCal Source command was executed.  The Go back in history command (Alt+LeftArrow) has the same effect when executed immediately after the Goto command.

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)

These commands jump to the previous or next (earlier or later in the module) use of the symbol selected by the most recent Show Uses command.

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.         *)
Such a box can be placed on a series of lines by itself, or it can appear to the right of other text. 

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  (***********************************

showing where the finished box will be positioned, and it leaves the cursor between them in the first column.  Type your comment like ordinary text, with all paragraph lines starting in column 1, like this:
Beauty == TRUE  (***********************************
This is 
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?
When you have finished the contents of the comment, execute the Format Comment command by typing Ctl+O Ctl+F.  This will format each sequence of non-blank lines that all begin in column 1 as a paragraph, with lines broken so the paragraphs will fit snugly in the comment box--like this: 
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?
Note that lines that do not begin in column 1 are not changed.  If it looks right, execute the Box Comment command by typing Ctl+O Ctl+B to create the box, like this:
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?           *)
If the result doesn't look right, type Ctl+Z to undo the Box Comment command and do whatever manual formatting seems necessary.  Then execute Box Comment again.  Both the formatting and the boxing can be done together with the Format and Box Comment command by typing Ctl+O Ctl+O.

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

Editor commands for hierarchically viewing proofs are described in Viewing Structured Proofs.  We hope eventually to provide commands to aid in writing and editing proofs.  We would appreciate any suggestions for what commands we should implement.  Meanwhile, block selection mode may be useful in copying and indenting parts of a proof.

Miscellaneous Commands

Goto Matching Parenthesis (Control+Shift+p)

Placing the cursor just to the right of a parenthesis and executing this command cause the cursor to jump to the right of the matching parenthesis.  The pairs of matching "parentheses" are:
     (  )    [  ]    {  }    <<  >>    (*  *)
The cursor does not move and an error message appears at the bottom left of the Toolbox window if there is no matching parenthesis or there are mismatched parentheses.  Mismatched parentheses are highlighted.  (Look to the right of the scroll bar to find them if they are off the screen.)  End-of-line comments (started with \*) and strings are treated as independent regions for parenthesis matching.

Toggle Block Selection Mode (Alt+Shift+a)

This command causes the editor to enter or leave block-selection mode.  In block-selection mode, you can select a rectangular region (which may have zero width).  You can delete, type into, or copy and paste the region.  Typing space or LeftArrow (backspace) into a zero-width region allows you to move a block of text left or right, which is useful for adjusting alignment.  In general, typing a single character into a zero-width region inserts that character on each line of the region. 

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

The following are the default key bindings for module editors.  The General/Keys item on the Preference menu allows you to change those key bindings.  Its Emacs scheme binds a few commands to the keys used in the Emacs editor, making the module editor almost, but not quite, completely unlike Emacs.

Insert, Delete, and Move Text
Ctl+Shift+Enter Insert line above current line
Shift+Enter Insert line below current line
Ctl+Shift+Del Delete to end of current line
Ctl+Backspace Delete to beginning of current or previous word
Ctl+Del Delete to end of current word
Alt+Up/DownArrow Move current line up/down
Shift+Tab If there are (at least) 4 spaces at beginning of line, delete them
Ctl+/ Comment out or uncomment selected lines
Ctl+Alt+J Join next line to current line
Ctl+C Copy selected text
Ctl+V Paste
Ctl+Z Undo
Ctl+A Select all
Alt+Shift+A Toggle block selection mode

Moving Around
For most of these commands, holding Shift down also selects the text.
Home/End Go to beginning/end of current line
Ctl+Home/End Go to beginning/end of module
Ctl+RightArrow Go to beginning of next word
Ctl+LeftArrow Go to beginning of current or previous word
Alt+RightArrow Go forward in history.
Alt+LeftArrow Go back in history.
Ctl+L Go to line [asks for line number]
Ctl+Q Go to last edit location
Ctl+Shift+P Go to matching parenthesis
Ctl+Up/DownArrow Scroll up/down one line
The arrow and page-up/down keys behave as usual.

Find and Replace
Ctl+F Raise Find/Replace dialog
Ctl+K Find next (in forward direction) instance of last search item
Ctl+Shift+K Find previous (in backwards direction) instance of last search item
Ctl+J Incremental forward find
Ctl+Shift+J Incremental backwards find

Finding Definitions and Declarations and Their Uses
F3 Goto declaration or definition
F4 Return from goto declaration or definition
F5 Show declarations and definitions
F6 Show uses of declaration or definition
F7 Goto previous use of declaration or definition
F7 Goto next use of declaration or definition

Editing Comments
Ctl+O Ctl+S Begin comment
Ctl+O Ctl+F Format comment
Ctl+O Ctl+B Box comment
Ctl+O Ctl+O Format and box comment
Ctl+O Ctl+U Unbox comment

Viewing Proofs
Ctl+G Ctl+S Show current subtree
Ctl+G Ctl+H Hide current subtree
Ctl+G Ctl+C Show children only
Ctl+G Ctl+F Focus on step
Ctl+G Ctl+A Show all proofs
Ctl+G Ctl+N Hide all proofs

Ctl+S Save module
Ctl+Shift+A Open Quick Access window
Alt+X Exit toolbox
Ctl+M Maximize or unmaximize current editor or view
Ctl+R Parse module
Ctl+Alt+R Parse spec
F1 Raise Help view
Ctl+PageUp/Down Go to previous/next editor view
Ctl+F6 Go to another editor view (Use up/down arrow to select view, then type Enter.)
Ctl+F7 Go to another view (Use up/down arrow to select view, then type Enter.)
Ctl+F10 Can use to set line-numbering preference or go to  Preferences /General/Editors/Text Editors

↑ Managing Your Specifications