Back - User Guide Index | Previous - The Formaliser Library | Next - Entering Specifications - Examples


Editor Overview

 

Basic Editor Structure

When you select to open a document for viewing and/or editing the document is loaded up into the editor window. This contains a menu bar at the top and two panes.

The top pane is called the production pane and contains the type of the currently highlighted section of the document then an arrow and a list of possible sub types available. The list of subtypes can be quite long so to scroll along the list you have to click and drag the cursor sideways.

The bottom pane displays the contents of the document.

Descriptions of each item in the editor menus are provided in the reference section.

 

Document Structure

The structure of a document is hierarchical and is held as a parse tree. Basically a document is a series of paragraphs each one representing a construct e.g. schema box, inline predicate, definition etc. Each of these are further broken down into their sub parts e.g. for a schema box you will have a schema name, basic declarations and predicates. The constructs are broken down until terminal nodes are reached e.g. infix operator symbol, variable, number etc.

A non-terminal node is broken down by being "instantiated". This is achieved by highlighting the node you wish to subdivide then either select "Instantiate" from the "Edit" menu or the pop up menu. This will display a list of possible constructs for the current node. Alternatively you can use the production pane and click on the type of construct you want; this will be to the right of the arrow. Note - non-terminal nodes are displayed within angle brackets e.g. <Predicate>.

Right-clicking on any node displays the pop up menu which contains a list of actions that are allowed on that node. The list of allowable actions will depend on type of the node.

Instead of instantiating a node down to its sub nodes you can type directly into the node. When you begin typing two diamond symbols appear to show the beginning and end of what you have entered. When you press enter the text it is parsed and only if it is syntactically correct will it allow it to be entered. If a parse error is encountered then a box will appear containing the text. It will indicate where the parse error has occurred and will give you the chance to edit the text before parsing it again or you can cancel the input.

 

Symbols and Identifiers

There are two ways in which to enter Z symbols. You can double click on a symbol in the symbol palette, this inserts the symbol at the current cursor position. You can also use keyboard shortcuts, a full list of these are supplied in the reference section. The shortcuts are transformed into the symbol by the parser.

Identifiers can be made up of characters that can be letters (alphabetic, digits, Greek and fat alphabetic e.g. ˆ ) or symbols (everything else). An identifier can be of the form - a sequence of letters (not beginning with a digit); a sequence of symbols; a sequence of letters and symbols but only if letters are separated from symbols by an underscore.