The Document Mark-Up Tool (dmu)

DocumentMarkUp (dmu) is invoked from the Documents Environment and is applicable to all constructs that have not been marked up (with the exception of `.ops' constructs).

The tool produces LaTeX source code (controlled through the Documents Option setting) - a source file named _constructname.tex written in the TEX directory - and the LaTeX Executable command issued.

The location of the executable (LaTeX or LaTeX2e) may be set in the LaTeX Executable option of the Documents Options (if not already in the PATH of the user); the default is latex.

The formatting of AMN constructs is automatic; the user may, however, dictate the style by the positioning of newlines/annotations in the document.

Note that the following comments do not apply to proof files; see Top Bar Help on ProofPrinter concerning the editing of proof files.

Comments and Annotations

The AMN source document may contain normal C-like comments:

   /* comment */

which are removed before processing.

However a special kind of comment - an annotation - is also permitted:

   /*" annotation "*/

Annotations are not discarded, but processed, and form an integral part of the end document, and so provide a means of complementing the formal mathematics of AMN documents with informal comment.

Annotations comprise LaTeX source code, and thus any LaTeX commands may be used inside an annotation, for example:

   /*" {\bf A bold statement}\\
   ... some annotation ... "*/

A single newline after the begin-annotation or preceding the end-annotation is not significant; thus the following annotations will appear the same in the printed document:

  /*" annotation "*/

  /*"
     annotation
  "*/

More that one newline in either position will result in more space appearing at that point in the document.

Annotations will normally be separated from the mathematical content in a document by horizontal lines; horizontal lines will not, however, appear around an empty annotation - one consisting entirely of white space (which may therefore be used to print vertical space) , or around an newpage annotation - one consisting of the command `\newpage' and optional white space (which will, of course, cause a newpage to be produced).

Positioning of Comments

Comments may appear anywhere in a document
Comments may not be nested
Comments may not appear inside annotations

Positioning of Newlines

Newlines may appear anywhere in a document, however only those detailed below are echoed in the LaTeX document.

Optional newlines may appear after the following construct keywords:

   MACHINE         REFINEMENT   IMPLEMENTATION  ENUMERATION
   SYSTEM          BASE         CONSTRAINTS
   USES            SEES         REFINES         INCLUDES
   IMPORTS         PROMOTES     EXTENDS         SETS
   CONSTANTS       PROPERTIES   VARIABLES       INVARIANT
   ASSERTIONS      DEFINITIONS  INITIALISATION  OPERATIONS

Each of the above keywords will always be preceded by a newline in the LaTeX document.

Optional newlines may appear before or after the following operation keywords:

   BEGIN   PRE   THEN    WHEN     IF        ELSE
   ELSIF   ANY   WHERE   SELECT   CASE      BE
   EITHER  OR    LET     CHOICE   IN        WHILE
   DO      VAR   OF      VARIANT  INVARIANT

The keyword END will always be preceded by a newline in the LaTeX document except when no newline appears in the following constructs:

   BEGIN ... END
   PRE ... THEN ... END
   IF ... THEN ... END
   IF ... THEN ... ELSE ... END
   ANY ... WHERE ... THEN ... END

Optional newlines may appear before or after any of the following symbols:

       &   ;   ,   ||   =   =>   <=>   or   :=

Breaking long lines may be achieved by the use of brackets; an open bracket immediately followed by a newline will cause a linebreak with all following lines being indented, and a closing bracket immediately preceded by a newline (followed by optional space characers) will stop the indentation. So a predicate written:
```
       xxx => (
       yyy 
        .
        .
        .
       zzz
       )
```
will be marked up with the consequent list indented as follows:
```
       xxx => (
         yyy 
          .
          .
          .
         zzz)
```
Note that if the brackets are unnecessary they will be discarded, although the linebreaking and indentation will still occur.
Multiple newlines are treated as a single newline

Rules Concerning Annotations

No white space should appear between annotation-defining characters / * ". For example:
```
       /* " annotation "*/
```
would be treated by the tool as a comment, and therefore discarded.
The start-annotation symbol /*" must appear at the beginning of a line
The end-annotation symbol "*/ must appear at the end of a line
Annotations may not be nested
Annotations may not appear inside a comment
Annotations may appear in the following positions:
- before or after each of the construct keywords listed above
- before or after after each of the operation keywords:
```
   THEN   WHEN  ELSE   ELSIF   WHERE  BE  OR  IN  OF
```
- after each of the operation keywords:
```
   BEGIN   PRE     IF     ANY  SELECT  CASE     EITHER 
   LET     CHOICE  WHILE  DO   VAR     VARIANT  INVARIANT
```
- before or after after each of the symbols:
```
           &   ;   ,   ||   :=
```
- If no annotation appears immediately preceding an operation, the operation name will be automatically printed in bold preceding the operation

A Special Annotation

An annotation appearing between the document name and the CONTENTS clause of a DOCUMENT is treated in a different way to other annotations: it is taken to be a prologue annotation, and will appear in the.texfile of the document immediately before the \begin{document}. This is to enable LaTeX commands specific to that document to be included (for example, the inclusion of a particular package through the \usepackage command. This prologue text may be set in the LaTeX Declaration of the Documents Options.

If LaTeX complains

Should your file fail to LaTeX correctly (for example if an annotation contains bad syntax) you should quit from LaTeX by typing `x' in the LaTeX window, edit the file, commit the edits and re-submit it for mark-up.

Note that the double quote character " inside an annotation causes the message `Bad annotation position' to be displayed (this is because annotations are represented internally as strings). Single quotes ` and ' may be used; if double quotes are required, `` and '' (double single quotes) should be used.

The Document Options

If the `Labels' option is set, the LaTeX commands \ref and \pageref may be used inside annotations to reference the occurrence of construct, variable, set, constant and operation names (for MACHINES, REFINEMENTS and IMPLEMENTATIONS)
If the `Clause cross-references' option is set, a cross-reference of external construct, variable, set, constant and operation names will automatically be produced after the PROPERTIES, INVARIANT ASSERTIONS, INITIALISATION clauses (if present) and following each operation (for MACHINES, REFINEMENTS and IMPLEMENTATIONS)
If the `Construct cross-references' option is set, a cross-reference of external construct, variable, set, constant and operation names will automatically be produced at the end of each MACHINE, REFINEMENT and IMPLEMENTATION
If the `Index' option is set, an index will be produced containing references to all construct, variable, set, constant and operation names at the end of each DOCUMENT

For a fuller explanation, see also Options.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo