to view the code in the Lava exec editor.Executable code is represented in the declaration tree by the keywords "Exec" and "Invariant/Require/Ensure". You may double-click these keywords or click the spectacles to view the code in the Lava exec editor.
The Lava exec view displays executable Lava code in a so-called "rich edit view" window as normal text, but the normal text editing functions are disabled and replaced by the so-called structure editing mode. Unlike normal text editing, structure editing allows you to select, insert, delete, replace, etc. only whole syntactic constructs (rather than individual characters). This fundamental difference would require some relearning but once you have understood its principles structure editing is much more productive and much less error-prone than traditional program development based on text editing.
You just select a Lava construct for insertion by clicking an associated tool button. You need not know its syntactical structure in advance: LavaPE will insert a "template" of that construct for you which exhibits its syntactical structure and contains placeholders for nested constructs that you may insert subsequently.
Optional parts of a construct can be deleted or reinserted if required.
Clicking a special insertion button or pressing the RETURN key causes an additional "empty" copy of a repeatable sub-construct to be inserted after or before the selected copy (depending on the current state of the "Insert before" button 
).
Advantages of Lava structure editing
Three types of Lava entities may or must be associated with executable code:
In the LavaPE tree view, execs and invariants are associated with a specific little icon 
which you may double-click to open the corresponding LavaPE exec view. Alternatively you may select the exec/invariant node of the declaration tree and then click the spectacles on the declaration bar to open the selected exec in a new exec view window.
Three specific toolbars belong to the Lava exec view:
The Exec switches toolbar
displaying various symbols of editing operations and of buttons that switch forth and back between different display modes and formats,
the Exec operations toolbar
displaying various Lava operators that can be used to construct Lava expressions and statements, and the vertical keyword toolbar, displaying the primary keywords of all Lava keyword constructs:
Basics of exec editingContext-sensitive help
Use the context-sensitive help of LavaPE to get information about individual menu items and operator and keyword tool buttons: Click the context help tool button 
, drag it to the respective Lava tool button or menu item for which you want to get an explanation and drop it there.
Pay attention to status bar hints
Depending on the current selection, the status bar will in many cases display hints on what you can do next. Lava beginners should pay attention to these hints.
How to insert/delete statements
If you have selected a statement placeholder <stm> and if you then click one of the enabled statement tool buttons then the placeholder is replaced with the corresponding statement template.
If you have selected an existing statement, rather than a placeholder, and if you then click one of the enabled statement tool buttons then the corresponding statement template is inserted after or before the selected statement, depending on the state of the "Insert before" tool button . If the selected statement was an operand of a logical conjunction (and / ;, or, xor) then the inserted statement is a new operand of the same logical conjunction. If the selected statement wasn't part of a conjunction then the inserted statement is connected by a logical "and / ;" conjunction to the selected statement.
If you have selected an existing statement or a placeholder and if you then click the "Insert" tool button 
or press the RETURN key then a new placeholder
<stm> is inserted after or before the selected statement, depending on the state of the "Insert before" tool button . The same rule as in the preceding paragraph applies to the logical conjunction that is used for the new placeholder.
If you have selected an existing (non-placeholder) statement and if you then click the "scissors" tool button 
then he selected statement is deleted and written to the clipboard if it was an operand of a logical conjunction; if it wasn't, then the statement is replaced with a <stm> placeholder in a first step; only if you attempt to delete the latter in turn the entire containing construct will be deleted.
If you press the DEL key instead of clicking the scissors then the statement is deleted but not written to the clipboard.
See also "Using the return key ...".
How to insert/delete expressions
If you have selected an existing expression or an expression placeholder <expr> and if you then click one of the enabled expression tool buttons from the operator or keywords toolbar then the expression/placeholder is replaced with the corresponding expression template.
If you have selected an existing expression or expression placeholder and if you then click the "Insert" tool button then a new placeholder
<expr> is inserted after or before the selected expression, depending on the state of the "Insert before" tool button . But note that for expressions the "Insert empty copy" button is only enabled if the selected expression is an operand of an operation supporting multiple operands, like "+" or "*". The inserted new placeholder is treated as an additional operand of this same operation.
If you have selected an existing expression and if you then click the "scissors" button then he selected expression is replaced with a placeholder
<expr> and written to the clipboard. If you press the DEL key instead then it is deleted but not written to the clipboard.
If you click the scissors or press the DEL key on an expression placeholder then the latter is deleted if the placeholder was an operand of a multiple operand operation; otherwise the entire containing construct is deleted.
See also "Using the return key ...".
How to insert/delete other kinds of repeatable constructs
Lava provides a number of constructs containing repeatable clauses other than statements and expressions, for instance the
elsif clauses of if statements and
ifx expressions, the case clauses of the
switch and type statements, and the quantifier clauses of the
declare, exists,
foreach, delete statements and of the
select expression. They all begin, except for the quantifiers, with a characteristic keyword which you can click to select the entire clause. You can delete the selected clause in the usual way using the scissors or the DEL key. You can click the "Insert empty copy" button to insert a new template of this kind of clauses after or before the selected clause, depending on the state of the "Insert before" tool button .
The quantifiers of declare don't contain any keyword that could be clicked to select the entire quantifier clause. As a substitute you can select the <type> placeholder or the specified concrete type reference that has replaced it before you click or or press DEL. In the delete case a type reference will be replaced with a
<type> placeholder in a first step before you can then delete the entire quantifier.
The other quantifiers, running through finite sets of objects, can be selected also by clicking their characteristic in keyword.
Every quantifier contains a list of one or several variables. You can use , , 
, and DEL in the obvious way for these.
See also "Using the return key ...".
How to insert/delete optional parts
Optional parts of a Lava construct begin with a purple keyword, for instance elsif, else, but, or where. By clicking this keyword and pressing the DEL button you can delete the optional part.
Select the Lava construct and click the "Show empty optionals" tool button 
to reinsert templates for all currently non-existing optional parts of that construct.
How to insert, edit and step through comments
The yellow balloon 
may be clicked to add or change a comment that is associated with the Lava construct that is currently selected in the exec view. The button 
may be used to toggle the visibility of comments in Lava execs. Comments are shown directly within the exec text, while in the tree view they are displayed in the comment page of the utility window if you select a commented tree node.
Error navigation
The two buttons 
may be used to open/close the error message window and to step from error to error in forward or backward direction. If you select a faulty (=red) construct then the first error message referring to that construct is displayed also in the status bar.
Cut/copy/paste
Cut/copy/paste work in the usual way, but for execs currently only within the same exec. Proper enabling/disabling of the corresponding buttons combined with subsequent checks that are performed anyway after each edit operation prevent syntactically inadmissible operations. Drag-and-drop, which is available in the declaration view, would be desirable also in the exec view. But its implementation is not quite easy and has been postponed so far.
Undo/Redo
Use the "Undo" and "Redo" buttons 
to undo or redo individual edit operations in any of the LavaPE views step by step on a "per document" basis. (Every document (= Lava file) has its own undo/redo memory.) The redo memory is deleted in the usual way after a new edit operation, the undo memory when the current document is saved.
Go to declaration / return to reference
You can double-click any reference to a Lava entity in an exec to jump to its declaration. Alternatively you can select the reference and click the "Go to declaration" button 
. Use the "Return to reference" button 
to follow the sequence of such "Go to declaration" operations in backward direction (= back to the locations from where you came). Both operations may jump forth and back between exec and declaration views and even between different ("included") Lava documents.
Using the arrow keys (up/down/left/right) to walk through the exec constructs
You can use the arrow keys to move the current selection through the nested exec constructs in up/down/left/right direction: "Cursor right/left" means to move the selection forth and back between "siblings" having the same containing ("parent") construct, for instance from statement to statement within the then part of an if statement. "Cursor up" means to move the selection to the containing ("parent") construct. "Cursor down" means to move the selection to the first child construct (if there is one).
How to open/close the little edit windows for constants and variable names
If the selection is on a constant or on a variable name (in the declaration of the variable) or on an <expr> or <varName> placeholder then "cursor down" opens a little edit window that allows you to edit the constant or the variable name. The same effect is achieved by double-clicking that item or by clicking the spectacles or by clicking again on the item after you have selected it.
You close a little edit window by pressing the return or ESC or "cursor up" key or by clicking on another construct outside the window.
Using the return key to insert another placeholder
If the selection is on any repeatable construct then you can press the return key to insert a placeholder for another construct of this same type, e.g., a statement placeholder <stm> if the selection is on a statement, an expression placeholder <expr> if it is on an expression, an elsif ... then clause if it is on elsif or then, a new quantifier if it is on the type name or on the <type> placeholder of an existing quantifier, a new local variable if it is on a variable name or on a <varName> placeholder in a declare, exists, foreach, or select construct.
Keyboard-centric editing of Lava execs
You can invoke the more important and frequent exec editing operations without using the mouse. Most of the keyword constructs can be inserted by pressing the underlined character of the keyword. For the operation toolbar, the tool tips on the status line tell you which character to use. You can use CTRL-1, CTRL-2, CTRL-3 to open the list box associated with the first, second, or third exec combo-box, and you can use the down and up arrow keys to step through the list items; finally you press the RETURN key to select the currently highlighted item. Use the arrow keys to navigate between parent, child, and sibling constructs as described above. Use the RETURN key to insert templates/placeholders for repeatable constructs.
Top-down, bottom-up, and mixed-order construction of arithmetic expressions
Expressions containing operators can be constructed in the standard top-down style of Lava exec editing, but also in bottom-up or mixed order. For instance, if you have already constructed "1 + 2" and you want to make this sum appear as the second factor of a product "<expr> * (1 + 2)", then just do the following:
. This causes the
<expr> to be inserted before the "1
+ 2".