Libraries.Text.PrettyPrint.Prettyprinter.Doc

Reexports

Definitions

textReplicateChar : Int -> Char -> String

Totality: total
Visibility: export

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:

Cast (Doc Void) (Doc ann)

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

replicateChar : Int -> Char -> Doc ann

  Repeat character `n` times.

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 Declaration: 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 -> Type

  Overloaded conversion to `Doc`.
  @ ann is the type of annotations
  @ a   is the type of things that can be prettified
  We declare that only `a` is relevant when looking for an implementation
  
  Pro tips:
  1. use `prettyBy` if a subprinter uses a different type of annotations
  2. use a variable `ann` rather than `Void` if no annnotation is needed
     (to avoid needless calls to `prettyBy absurd`)

Parameters: ann, a
Methods:

pretty : a -> Doc ann

prettyPrec : Prec -> a -> Doc ann

Implementations:

Pretty Void Token

Pretty Void PkgVersion

Pretty Void PkgVersionBounds

Pretty Void Depends

Pretty Void PkgDesc

Pretty IdrisDocAnn CDef

Pretty IdrisSyntax (NamedPats todo vars)

Pretty IdrisSyntax (PatClause todo vars)

Pretty Void SExpToken

Pretty IdrisSyntax Premise

Pretty Void StopReason

Pretty Void Token

Pretty i a => Pretty i (WithFC a)

Pretty IdrisSyntax (BasicMultiBinder' KindedName)

Pretty IdrisSyntax (PBinder' KindedName)

Pretty IdrisSyntax IPTerm

Pretty Void REPLEval

Pretty Void REPLOpt

Pretty IdrisSyntax Pat

Pretty ann DotReason

Pretty Void FC

Pretty IdrisSyntax PrimType

Pretty IdrisSyntax Constant

Pretty Void Visibility

Pretty Void PartialReason

Pretty Void Terminating

Pretty Void Covering

Pretty Void Totality

Pretty Void Namespace

Pretty Void ModuleIdent

Pretty Void UserName

Pretty Void Name

Pretty Void String

Pretty Void Char

Pretty Void SizeChange

pretty : Pretty ann a => a -> Doc ann

Totality: total
Visibility: public export

prettyPrec : Pretty ann a => Prec -> a -> Doc ann

Totality: total
Visibility: public export

prettyBy : Pretty ann1 a => (ann1 -> ann2) -> a -> Doc ann2

  Sometimes we want to call a subprinter that uses a different annotation
  type. That's fine as long as we know how to embed such annotations into
  the target ones.
  @ ann1 is the type of annotations used by the subprinter
  @ ann2 is the type of annotations used in the current document
  @ inj  explains how to inject the first into the second

Totality: total
Visibility: export

pretty0 : Pretty Void a => a -> Doc ann

  Sometimes we want to call a subprinter that uses no annotation whatsoever.
  This should be equivalent to `prettyBy absurd`, except that in this case
  we do not traverse the document because it should be impossible to manufacture
  an annotation of type Void.

Totality: total
Visibility: export

byShow : Show a => a -> Doc ann

Totality: total
Visibility: export

commaSep : List (Doc ann) -> Doc ann

Totality: total
Visibility: 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

prettyList : Pretty ann a => List a -> Doc ann

Totality: total
Visibility: export

prettyList1 : Pretty ann a => List1 a -> Doc ann

Totality: total
Visibility: export

prettyMaybe : Pretty ann a => Maybe a -> Doc ann

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

displaySpans : SimpleDocStream a -> (String, List (Span a))

Totality: total
Visibility: export