The structure Fmt provides a mechanism for generic textual
formatting resp. "pretty printing". See also FmtDebug
for functions in the style of structure DEBUG working on
formats ( FmtDebug), FmtSeq for formatting
sequences ( FmtSeq), FmtOption for formatting
option types and FmtBasicTypes for formatting basic types.
List of Import References :
See BOOL
See Char
See DENOTATION
See Nat
See Option
See Seq
See String
See Void
SIGNATURE Fmt
$Date: 2012-10-02 14:17:54 +0200 (Di, 02. Okt 2012) $ ($Revision: 838 $)
IMPORT Void ONLY void Nat ONLY nat String ONLY string Seq[denotation] ONLY seq Seq[string] ONLY seq Seq[fmt] ONLY seq
The sort of possible formats is opaque:
SORT fmt
These functions provide a more graphical and functional interface to the pretty printer.
White space is not output when the last literal ended with space, when the last action output white space or at the beginning of a new line. It is mapped to a single line break when the right margin is reached.
There are two general kinds of literals supported. The first is considered to be atomic and can not be broken down under any circumstances. The second is considered to consist of tokens and white space, where the white space seperates the tokens but is not treated literally, and the whole literal may be broken down to tokens at any point.
For glued blocks, the first parameter specifies the indentation used when the block must be broken down to pieces. The unbreakable block needs no indentation, for obvious reasons.
FUN <> : fmt -- empty output <_> : fmt -- white space (usually one blank) <__> : nat -> fmt -- white space (usually N blanks) <~> : fmt -- single literal blank |<<- : fmt -- force new line ->| : fmt -- tabulator (every 8 columns) ->! : nat -> fmt -- proceed to specified column (1 .. margin) x : fmt ** nat -> fmt -- n-fold repetition ! : denotation -> fmt -- denotation, unbreakable !- : denotation -> fmt -- denotation, \t and \n recognized !_ : denotation -> fmt -- tokenized denotation, breakable !! : string -> fmt -- string, unbreakable !!- : string -> fmt -- string, \t and \n recognized !!_ : string -> fmt -- tokenized string, breakable .. : fmt ** fmt -> fmt -- concatenation ..* : seq[fmt] -> fmt -- n-fold concatenation ..|..* : fmt ** seq[fmt] -> fmt -- same with interleaving output >.< : fmt ** fmt -> fmt -- glued block (weak) >>.< : fmt ** fmt -> fmt -- glued block (moderate) >>>.< : fmt ** fmt -> fmt -- glued block (strong) >>>>.< : fmt -> fmt -- glued block (unbreakable) |.| : fmt ** fmt -> fmt -- add indentation for block |! : fmt -> fmt -- indent block to current column
These functions provide a more descriptive and imperative interface to the pretty printer.
Functions of both interfaces may be used at any time and even mixed up. However, you are encouraged to stick to one variant.
COMPATIBILITY NOTE: The behaviour of spc(N) differs slightly from the previous implementation. If the previously output character was a blank then no blanks are output. In practice, such cases should rarely occur and are easily corrected.
FUN none : fmt -- empty output spc : nat -> fmt -- white space (usually N blanks) brk : fmt -- force new line lit : denotation -> fmt -- denotation, \t and \n recognized lit : string -> fmt -- string, \t and \n recognized ; : fmt ** fmt -> fmt -- concatenation beg : nat -> fmt -- begin strong glued block,set break indent end : fmt -- end glued block block : nat ** fmt -> fmt -- glued block, set indentation on break inc : nat -> fmt -- increase left margin dec : nat -> fmt -- decrease left margin
These functions generate output from a given format.
The full interface allows for specification of the initial indentation (arbitrary format or left margin (1 .. margin)), the right margin (left_margin .. max_columns) and the format to be output. A sequence of strings is returned, each representing one physical line and not terminated by a newline character.
A second pair of functions provides the same functionality, but returns a single string where a newline character is appended to every line including the last.
For convenience, two more functions are provided, which assume columns 1 to 70 and return a single string or denotation.
FUN pretty : fmt ** nat ** fmt -> seq[string] pretty : nat ** nat ** fmt -> seq[string] pretty : fmt ** nat ** fmt -> string pretty : nat ** nat ** fmt -> string pretty : fmt -> string pretty : fmt -> denotation
next node: FmtBasicTypes,
prev node: Subsystem Formatting Tools,
up to node: Subsystem Formatting Tools