Text.PrettyPrint.Bernardy.Core

Definitions

data NonEmptySnoc : SnocList a -> Type

Totality: total
Visibility: public export
Constructor: 

IsNonEmptySnoc : NonEmptySnoc (sx :< x)

record LayoutOpts : Type

Totality: total
Visibility: public export
Constructor: 

Opts : Nat -> LayoutOpts

Projection: 

.lineLength : LayoutOpts -> Nat

Hint: 

FromString (Doc opts)

.lineLength : LayoutOpts -> Nat

Totality: total
Visibility: public export

lineLength : LayoutOpts -> Nat

Totality: total
Visibility: public export

record Layout : Type

Totality: total
Visibility: export
Constructor: 

MkLayout : (content : Lazy (SnocList String)) -> Stats -> {auto 0 _ : NonEmptySnoc (Force content)} -> Layout

Projections:

.content : Layout -> Lazy (SnocList String)

0 .prfNonEmptyContent : ({rec:0} : Layout) -> NonEmptySnoc (Force (content {rec:0}))

.stats : Layout -> Stats

Hints:

FromString Layout

Monoid Layout

Semigroup Layout

height : Layout -> Nat

  Returns the number of lines in a `Layout`.

Totality: total
Visibility: export

isMultiline : Layout -> Bool

  Returns the number of lines in a `Layout`.

Totality: total
Visibility: export

width : Layout -> Nat

  Returns the width of the longest line in a `Layout`

Totality: total
Visibility: export

isEmpty : Layout -> Bool

Totality: total
Visibility: export

empty : Layout

  The empty layout, consisting of a single empty line.

Totality: total
Visibility: export

render : Layout -> String

  Render the given layout

Totality: total
Visibility: export

line : String -> Layout

  Convert a single line of text to a layout.
  
  @ str this must be single line of text.

Totality: total
Visibility: export

text : String -> Layout

  Convert a string to a layout.
  This preserves any manual formatting
  
  @ str the String to pretty print

Totality: total
Visibility: export

flush : Layout -> Layout

Totality: total
Visibility: export

indent : Nat -> Layout -> Layout

Totality: total
Visibility: export

record Doc : LayoutOpts -> Type

  A non-empty selection of possible layouts.

Totality: total
Visibility: export
Constructor: 

MkDoc : Layout -> List Layout -> Doc opts

Projections:

.head : Doc opts -> Layout

.tail : Doc opts -> List Layout

Hint: 

FromString (Doc opts)

pure : Layout -> Doc opts

Totality: total
Visibility: export

render : (opts : LayoutOpts) -> Doc opts -> String

  Render the best candidate from the given set of layouts

Totality: total
Visibility: export

(<|>) : Doc opts -> Doc opts -> Doc opts

  Choose the better of two different documents.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 2

(<+>) : Doc opts -> Doc opts -> Doc opts

  Concatenate two documents horizontally.
  
  The first line of the second document will be appended
  to the last line of the first, and the remaining lines
  of the second will be indented accordingly.
  
  For instance, for documents `x` and `y` of the following
  shapes
  
  ```
  xxxxxxxxxxx
  xxxxxxxxxxxxxx
  xxx
  ```
  and
  
  ```
  yyyyy
  yy
  yyyy
  ```
  the result will be aligned as follows:
  
  ```
  xxxxxxxxxxx
  xxxxxxxxxxxxxx
  xxxyyyyy
     yy
     yyyy
  ```

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 8

empty : Doc opts

  The empty document, consisting of a single emtpy line.

Totality: total
Visibility: export

(>>=) : Doc opts -> (Layout -> Doc opts) -> Doc opts

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 1

line : String -> Doc opts

  Creates a single-line document from the given string.
  
  @str A string without line breaks

Totality: total
Visibility: export

flush : Doc opts -> Doc opts

  Flushes the last line of the given document, so that an appended
  document starts on a new line.

Totality: total
Visibility: export

indent : Nat -> Doc opts -> Doc opts

  Indents the given document by a number of spaces.

Totality: total
Visibility: export

indent' : Nat -> Doc opts -> Doc opts

  Indents the given document by a number of spaces, if it's not empty.

Totality: total
Visibility: export

text : String -> Doc opts

  Displays a single string, preserving any manual formatting.

Totality: total
Visibility: export