A label annotation is of the form `%[ID,...,ID]'. It is written in any semicolon- or bullet-separated list of items, immediately preceding the item to which it is to be attached.
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>÷%!
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.
An explicit `<other>' part can be used to provide abbreviations, e.g.,
... VLSI %!<other>Very_Long_Simple_Identifier%!
The input symbol whose display is to be affected may also be indicated explicitly in the display annotation, which may then be inserted at any point in a CASL specification, e.g.,
... %! div<latex>$\div$<html>÷%!
(The space following the opening `%!' is optional, except when the input symbol starts with a `<'.)
The notation for display annotations with implicit input symbols could be made more concise by letting <latex> be implied by an initial `$' or `\', and <html> be implied by an initial `&'. E.g.,
... div %!$\div$ ÷%!
Note that readability is not a crucial issue here, since display annotations are not themselves to be displayed, and can be seen only when using an editor on the input syntax.
Finally, display annotations generalize to formatting mixfix notation by interpreting the place-holder `__' as such in the formatting instructions, e.g.,
... sum__to__ %!<latex>\sum_{__}^{__}<html>SUM<sub>__<sup>__%!
This indicates the display not only for the mixfix operation symbol per se, but also for its application to argument terms (the place-holders being replaced by the arguments in the same order as input). If needed, LaTeX-style notation for argument positions `#n' could be provided too.
These annotations, applicable to an entire library, are to allow users to specify the precedence of operation symbols, and the significance of layout in the so-called "offside" rule. Their primary purpose is to allow the omission of grouping parentheses and/or list separators in the input; but formatters may also exploit them to avoid superfluous parentheses in the display. An approved set of parsing annotations and their syntax have yet to be worked out.