This module contains a document data type Doc for displaying (heterogenous) CASL specifications at least as plain text and latex (and maybe html as well)

Inspired by John Hughes's and Simon Peyton Jones's Pretty Printer Combinators in Text.PrettyPrint.HughesPJ, Thomas Hallgren's PrettyDoc within programatica, Daan Leijen's PPrint: A prettier printer 2001, and Olaf Chiti's Pretty printing with lazy Dequeues 2003

The main combinators are those of HughesPJ except nest, hang and $$. Instead of $$ $+$ must be used that always forces a line break. Indentation must be constructed using <> or <+>, i.e. text "spec" <+> MultilineBlock.

Also char, ptext, int, integer, float, double and rational do not exist. These can all be simulated using text (and show). There's an instance for Int in Common.DocUtils.

Furthermore, documents can no longer be tested with isEmpty. empty documents are silently ignored (as by HughesPJ) and often it is more natural (or even necessary anyway) to test the original data structure for emptiness.

Putting a document into braces should be done using specBraces (but a function braces is also exported), ensuring that opening and closing braces are in the same column if the whole document does not fit on a single line.

Rendering of documents is achieved by translations to the old Common.Lib.Pretty. For plain text simply show can be used. Any document can be translated to LaTeX via toLatex and then processed further by Common.PrintLaTeX. If you like the output is a different question, but the result should be legal LaTeX in conjunction with the hetcasl.sty file.

For nicer looking LaTeX the predefined symbol constants should be used! There is a difference between bullet and dot that is not visible in plain text.

There are also three kinds of keywords, a plain keyword, a topSigKey having the width of "preds", and a topKey having the width of "view". In plain text only inserted spaces are visible.

Strings in small caps are created by structId and indexed. The latter puts the string also into a LaTeX index.

In order to avoid considering display annotations and precedences, documents can be constructed using annoDoc, idDoc, and idApplDoc.

Currently only a few annotations (i.e. labels and %implied) are printed flushRight. This function is problematic as it does not prevent something to be appended using <> or <+>. Furthermore flushed parts are currently only visible in plain text, if they don't fit on the same line (as nest is used for indenting).

Further functions are documented in Common.DocUtils.

Examples can be produced using: hets -v2 -o pp.dol,pp.tex