Agda.Syntax.Common.Pretty

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.

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

Separate, but only if both separees are not null.

Apply parens to Doc if boolean is true.

Handles strings with newlines properly (preserving indentation)

Only wrap in parens if not empty

Used for with-like telescopes

Pretty print a single association.

Comma separated list, without the brackets.

Pretty print an association list.

Pretty print a set.

Use instead of show when printing to world.

Return empty for empty strings.

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

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 ....

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.

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

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

Attach an annotation to a document.

Either hcat or vcat.

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

"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.

Returns True if the document is 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 <>.

Same as text. Used to be used for Bytestrings.

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

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).

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.

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

Rendering mode.

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.

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.

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!