Idris2Doc : Text.PrettyPrint.Prettyprinter.Doc

Text.PrettyPrint.Prettyprinter.Doc

Reexports

import public Data.List1
import public Data.String.Extra

Definitions

textSpaces : Int -> String
Totality: total
Visibility: export
data PageWidth : Type
  Maximum number of characters that fit in one line.

Totality: total
Visibility: public export
Constructors:
AvailablePerLine : Int -> Double -> PageWidth
  The `Int` is the number of characters, including whitespace, that fit in a line.
The `Double` is the ribbon, the fraction of the toal page width that can be printed on.
Unbounded : PageWidth
  The layouters should not introduce line breaks.
data FusionDepth : Type
  Fusion depth parameter.

Totality: total
Visibility: public export
Constructors:
Shallow : FusionDepth
  Do not dive deep into nested documents.
Deep : FusionDepth
  Recurse into all parts of the `Doc`. May impact performace.
data Doc : Type -> Type
  This data type represents pretty documents that have
been annotated with an arbitrary data type `ann`.

Totality: total
Visibility: public export
Constructors:
Empty : Doc ann
Chara : Char -> Doc ann
Text : Int -> String -> Doc ann
Line : Doc ann
FlatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
Cat : Doc ann -> Doc ann -> Doc ann
Nest : Int -> Doc ann -> Doc ann
Union : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
Column : (Int -> Doc ann) -> Doc ann
WithPageWidth : (PageWidth -> Doc ann) -> Doc ann
Nesting : (Int -> Doc ann) -> Doc ann
Annotated : ann -> Doc ann -> Doc ann

Hints:
FromString (Doc ann)
Functor Doc
Monoid (Doc ann)
Semigroup (Doc ann)
Show (Doc ann)
column : (Int -> Doc ann) -> Doc ann
  Layout a document depending on which column it starts at.

Totality: total
Visibility: export
nest : Int -> Doc ann -> Doc ann
  Lays out a document with the current nesting level increased by `i`.

Totality: total
Visibility: export
nesting : (Int -> Doc ann) -> Doc ann
  Layout a document depending on the current nesting level.

Totality: total
Visibility: export
width : Doc ann -> (Int -> Doc ann) -> Doc ann
  Lays out a document, and makes the column width of it available to a function.

Totality: total
Visibility: export
pageWidth : (PageWidth -> Doc ann) -> Doc ann
  Layout a document depending on the page width, if one has been specified.

Totality: total
Visibility: export
align : Doc ann -> Doc ann
  Lays out a document with the nesting level set to the current column.

Totality: total
Visibility: export
hang : Int -> Doc ann -> Doc ann
  Lays out a document with a nesting level set to the current column plus `i`.
Negative values are allowed, and decrease the nesting level accordingly.

Totality: total
Visibility: export
spaces : Int -> Doc ann
  Insert a number of spaces.

Totality: total
Visibility: export
indent : Int -> Doc ann -> Doc ann
  Indents a document with `i` spaces, starting from the current cursor position.

Totality: total
Visibility: export
fill : Int -> Doc ann -> Doc ann
  Lays out a document. It then appends spaces until the width is equal to `i`.
If the width is already larger, nothing is appended.

Totality: total
Visibility: export
(<++>) : Doc ann -> Doc ann -> Doc ann
  Concatenates two documents with a space in between.

Totality: total
Visibility: export
Fixity Declarations:
infix operator, level 5
infixr operator, level 5
infixr operator, level 6
emptyDoc : Doc ann
  The empty document behaves like `pretty ""`, so it has a height of 1.

Totality: total
Visibility: export
softline : Doc ann
  Behaves like `space` if the resulting output fits the page, otherwise like `line`.

Totality: total
Visibility: export
softline' : Doc ann
  Like `softline`, but behaves like `neutral` if the resulting output does not fit
on the page.

Totality: total
Visibility: export
hardline : Doc ann
  A line break, even when grouped.

Totality: total
Visibility: export
group : Doc ann -> Doc ann
  Tries laying out a document into a single line by removing the contained
line breaks; if this does not fit the page, or has an `hardline`, the document
is laid out without changes.

Totality: total
Visibility: export
flatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
  By default renders the first document, When grouped renders the second, with
the first as fallback when there is not enough space.

Totality: total
Visibility: export
line : Doc ann
  Advances to the next line and indents to the current nesting level.

Totality: total
Visibility: export
line' : Doc ann
  Like `line`, but behaves like `neutral` if the line break is undone by `group`.

Totality: total
Visibility: export
fillBreak : Int -> Doc ann -> Doc ann
  First lays out the document. It then appends spaces until the width is equal to `i`.
If the width is already larger than `i`, the nesting level is decreased by `i`
and a line is appended.

Totality: total
Visibility: export
concatWith : (Doc ann -> Doc ann -> Doc ann) -> List (Doc ann) -> Doc ann
  Concatenate all documents element-wise with a binary function.

Totality: total
Visibility: export
hsep : List (Doc ann) -> Doc ann
  Concatenates all documents horizontally with `(<++>)`.

Totality: total
Visibility: export
vsep : List (Doc ann) -> Doc ann
  Concatenates all documents above each other. If a `group` undoes the line breaks,
the documents are separated with a space instead.

Totality: total
Visibility: export
fillSep : List (Doc ann) -> Doc ann
  Concatenates the documents horizontally with `(<++>)` as long as it fits the page,
then inserts a line and continues.

Totality: total
Visibility: export
sep : List (Doc ann) -> Doc ann
  Tries laying out the documents separated with spaces and if this does not fit,
separates them with newlines.

Totality: total
Visibility: export
hcat : List (Doc ann) -> Doc ann
  Concatenates all documents horizontally with `(<+>)`.

Totality: total
Visibility: export
vcat : List (Doc ann) -> Doc ann
  Vertically concatenates the documents. If it is grouped, the line breaks are removed.

Totality: total
Visibility: export
fillCat : List (Doc ann) -> Doc ann
  Concatenates documents horizontally with `(<+>)` as log as it fits the page, then
inserts a line and continues.

Totality: total
Visibility: export
cat : List (Doc ann) -> Doc ann
  Tries laying out the documents separated with nothing, and if it does not fit the page,
separates them with newlines.

Totality: total
Visibility: export
punctuate : Doc ann -> List (Doc ann) -> List (Doc ann)
  Appends `p` to all but the last document.

Totality: total
Visibility: export
plural : Num amount => Eq amount => doc -> doc -> amount -> doc
Totality: total
Visibility: export
enclose : Doc ann -> Doc ann -> Doc ann -> Doc ann
  Encloses the document between two other documents using `(<+>)`.

Totality: total
Visibility: export
surround : Doc ann -> Doc ann -> Doc ann -> Doc ann
  Reordering of `encloses`.
Example: concatWith (surround (pretty ".")) [pretty "Text", pretty "PrettyPrint", pretty "Doc"]
Text.PrettyPrint.Doc

Totality: total
Visibility: export
encloseSep : Doc ann -> Doc ann -> Doc ann -> List (Doc ann) -> Doc ann
  Concatenates the documents separated by `s` and encloses the resulting document by `l` and `r`.

Totality: total
Visibility: export
annotate : ann -> Doc ann -> Doc ann
  Adds an annotation to a document.

Totality: total
Visibility: export
alterAnnotations : (ann -> List ann') -> Doc ann -> Doc ann'
  Changes the annotations of a document. Individual annotations can be removed,
changed, or replaced by multiple ones.

Totality: total
Visibility: export
unAnnotate : Doc ann -> Doc xxx
  Removes all annotations.

Totality: total
Visibility: export
reAnnotate : (ann -> ann') -> Doc ann -> Doc ann'
  Changes the annotations of a document.

Totality: total
Visibility: export
interface Pretty : Type -> Type
  Overloaded conversion to `Doc`.

Parameters: a
Methods:
pretty : a -> Doc ann
prettyPrec : Prec -> a -> Doc ann

Implementations:
Pretty String
Pretty a => Pretty (List a)
Pretty a => Pretty (List1 a)
Pretty ()
Pretty Bool
Pretty Char
Pretty Nat
Pretty Int
Pretty Integer
Pretty Double
Pretty Bits8
Pretty Bits16
Pretty Bits32
Pretty Bits64
Pretty Int8
Pretty Int16
Pretty Int32
Pretty Int64
(Pretty a, Pretty b) => Pretty (a, b)
Pretty a => Pretty (Maybe a)
Pretty StopReason
pretty : Pretty a => a -> Doc ann
Totality: total
Visibility: public export
prettyPrec : Pretty a => Prec -> a -> Doc ann
Totality: total
Visibility: public export
list : List (Doc ann) -> Doc ann
  Variant of `encloseSep` with braces and comma as separator.

Totality: total
Visibility: export
tupled : List (Doc ann) -> Doc ann
  Variant of `encloseSep` with parentheses and comma as separator.

Totality: total
Visibility: export
fuse : FusionDepth -> Doc ann -> Doc ann
  Combines text nodes so they can be rendered more efficiently.

Totality: total
Visibility: export
data SimpleDocStream : Type -> Type
  This data type represents laid out documents and is used by the display functions.

Totality: total
Visibility: public export
Constructors:
SEmpty : SimpleDocStream ann
SChar : Char -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
SText : Int -> String -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
SLine : Int -> SimpleDocStream ann -> SimpleDocStream ann
SAnnPush : ann -> SimpleDocStream ann -> SimpleDocStream ann
SAnnPop : SimpleDocStream ann -> SimpleDocStream ann

Hint: 
Functor SimpleDocStream
alterAnnotationsS : (ann -> Maybe ann') -> SimpleDocStream ann -> SimpleDocStream ann'
  Changes the annotation of a document to a different annotation or none.

Totality: total
Visibility: export
unAnnotateS : SimpleDocStream ann -> SimpleDocStream xxx
  Removes all annotations.

Totality: total
Visibility: export
reAnnotateS : (ann -> ann') -> SimpleDocStream ann -> SimpleDocStream ann'
  Changes the annotation of a document.

Totality: total
Visibility: export
collectAnnotations : Monoid m => (ann -> m) -> SimpleDocStream ann -> m
  Collects all annotations from a document.

Totality: total
Visibility: export
traverse : Applicative f => (ann -> f ann') -> SimpleDocStream ann -> f (SimpleDocStream ann')
  Transform a document based on its annotations.

Totality: total
Visibility: export
removeTrailingWhitespace : SimpleDocStream ann -> SimpleDocStream ann
  Removes all trailing space characters.

Totality: total
Visibility: export
FittingPredicate : Type -> Type
Totality: total
Visibility: public export
defaultPageWidth : PageWidth
Totality: total
Visibility: export
record LayoutOptions : Type
Totality: total
Visibility: public export
Constructor: 
MkLayoutOptions : PageWidth -> LayoutOptions

Projection: 
.layoutPageWidth : LayoutOptions -> PageWidth
.layoutPageWidth : LayoutOptions -> PageWidth
Totality: total
Visibility: public export
layoutPageWidth : LayoutOptions -> PageWidth
Totality: total
Visibility: public export
defaultLayoutOptions : LayoutOptions
Totality: total
Visibility: export
layoutWadlerLeijen : FittingPredicate ann -> PageWidth -> Doc ann -> SimpleDocStream ann
  The Wadler/Leijen layout algorithm.

Totality: total
Visibility: export
layoutUnbounded : Doc ann -> SimpleDocStream ann
  Layout a document with unbounded page width.

Totality: total
Visibility: export
layoutPretty : LayoutOptions -> Doc ann -> SimpleDocStream ann
  The default layout algorithm.

Totality: total
Visibility: export
layoutSmart : LayoutOptions -> Doc ann -> SimpleDocStream ann
  Layout algorithm with more lookahead than layoutPretty.

Totality: total
Visibility: export
layoutCompact : Doc ann -> SimpleDocStream ann
  Lays out the document without adding any indentation. This layouter is very fast.

Totality: total
Visibility: export
renderShow : SimpleDocStream ann -> String -> String
Totality: total
Visibility: export