Agda.Syntax.Common.Pretty

While Show is for rendering data in Haskell syntax, Pretty is for displaying data to the world, i.e., the user and the environment.

Atomic data has no inner document structure, so just implement pretty as pretty a = text $ ... a ....

Use instead of show when printing to world.

The type of documents. We use documents annotated by Aspects to record syntactic highlighting information that is generated during pretty-printing.

Comma separated list, without the brackets.

align max rows lays out the elements of rows in two columns, with the second components aligned. The alignment column of the second components is at most max characters to the right of the left-most column.

Precondition: max > 0.

Pretty print a set.

Pretty print an association list.

Separate, but only if both separees are not null.

Pretty print a single association.

Apply parens to Doc if boolean is true.

Only wrap in parens if not empty

Handles strings with newlines properly (preserving indentation)

Used for with-like telescopes

Attach a simple Aspect, rather than a full set of Aspects, to a document.

A document of height 1 containing a literal string. text satisfies the following laws:

• text s <> text t = text (s++t)

• text "" <> x = x, if x non-empty

The side condition on the last law is necessary because text "" has height 1, while empty has no height.

Render the Doc to a String using the default Style (see style).

A document of height and width 1, containing a literal character.

Rendering mode.

Returns True if the document is empty

Beside, separated by space, unless one of the arguments is empty. <+> is associative, with identity empty.

Either hcat or vcat.

Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:

   text "hi" $$ nest 5 (text "there")

lays out as

   hi   there

rather than

   hi
        there

$$ is associative, with identity empty, and also satisfies

• (x $$ y) <> z = x $$ (y <> z), if y non-empty.

Attach an annotation to a document.

Above, with no overlapping. $+$ is associative, with identity empty.

Nest (or indent) a document by a given number of positions (which may also be negative). nest satisfies the laws:

• nest 0 x = x

• nest k (nest k' x) = nest (k+k') x

• nest k (x <> y) = nest k z <> nest k y

• nest k (x $$ y) = nest k x $$ nest k y

• nest k empty = empty

• x <> nest k y = x <> y, if x non-empty

The side condition on the last law is needed because empty is a left identity for <>.

A rendering style. Allows us to specify constraints to choose among the many different rendering options.

A single Char fragment

Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.

A Span represents the result of an annotation after a Doc has been rendered, capturing where the annotation now starts and ends in the rendered output.

"Paragraph fill" version of cat.

The general rendering interface. Please refer to the Style and Mode types for a description of rendering mode, line length and ribbons.

The general rendering interface, supporting annotations. Please refer to the Style and Mode types for a description of rendering mode, line length and ribbons.

Same as text. Used to be used for Bytestrings.

Render an annotated Doc to a String and list of annotations (see Span) using the default Style (see style).

Render the Doc to a String using the given Style.

Some text with any width. (text s = sizedText (length s) s)

The default style (mode=PageMode, lineLength=100, ribbonsPerLine=1.5).

Some text, but without any width. Use for non-printing text such as a HTML or Latex tags

An associative operation.

Examples

>>> [1,2,3] <> [4,5,6][1,2,3,4,5,6]

>>> Just [1, 2, 3] <> Just [4, 5, 6]Just [1,2,3,4,5,6]

>>> putStr "Hello, " <> putStrLn "World!"Hello, World!