Prev Up Next
Go backward to C.5.2.1 Label Annotations
Go up to C.5.2 Annotations
Go forward to C.5.2.3 Parsing Annotations

C.5.2.2 Display Annotations

A display annotation is of the form `%!...%!'. It associates a particular input symbol (an ID) with formatting instructions for its display, using the same notation for delimiting formatting languages as used for comments.

When the display annotation immediately follows a declared ID in a sort, operation, or variable declaration, the input symbol concerned is taken to be that ID, and the body of the display annotation gives the formatting instructions. E.g.,

... div %!<latex>$\div$<html>&divide;%!
determines how the ID input as `div' is to be displayed by LaTeX and HTML formatters (÷), with other formatters by default displaying the input symbol as written.

Further details concerning the use of formatting instructions in annotations are given in [BCKB+98].

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to

Prev Up Next