Init.Data.Format.Basic

source

inductive Std.Format.FlattenBehavior :

Type

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

allOrNone will make a linebreak on every Format.line in the group or none of them.
```
[1,
 2,
 3]
```
fill will only make linebreaks on as few Format.lines as possible:
```
[1, 2,
 3]
```

allOrNone: Std.Format.FlattenBehavior
fill: Std.Format.FlattenBehavior

Instances For

source

instance Std.Format.instInhabitedFlattenBehavior :

Inhabited Std.Format.FlattenBehavior

Equations

Std.Format.instInhabitedFlattenBehavior = { default := Std.Format.FlattenBehavior.allOrNone }

source

instance Std.Format.instBEqFlattenBehavior :

BEq Std.Format.FlattenBehavior

Equations

Std.Format.instBEqFlattenBehavior = { beq := Std.Format.beqFlattenBehavior✝ }

source

inductive Std.Format :

Type

A string with pretty-printing information for rendering in a column-width-aware way.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

nil: Lean.Format
The empty format.
line: Lean.Format
A position where a newline may be inserted if the current group does not fit within the allotted column width.
align: Bool → Lean.Format
align tells the formatter to pad with spaces to the current indent, or else add a newline if we are already at or past the indent. For example:
```
nest 2 <| "." ++ align ++ "a" ++ line ++ "b"
```
results in:
```
. a
  b
```
If force is true, then it will pad to the indent even if it is in a flattened group.
text: String → Lean.Format
A node containing a plain string.
nest: Int → Lean.Format → Lean.Format
nest n f tells the formatter that f is nested inside something with length n so that it is pretty-printed with the correct indentation on a line break. For example, we can define a formatter for list l : List Format as:
```
let f := join <| l.intersperse <| ", " ++ Format.line
group (nest 1 <| "[" ++ f ++ "]")
```
This will be written all on one line, but if the text is too large, the formatter will put in linebreaks after the commas and indent later lines by 1.
append: Lean.Format → Lean.Format → Lean.Format
Concatenation of two Formats.
group: Lean.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Lean.Format
Creates a new flattening group for the given inner format.
tag: Nat → Lean.Format → Lean.Format
Used for associating auxiliary information (e.g. Exprs) with Format objects.

Instances For

source

instance Std.instInhabitedFormat :

Inhabited Lean.Format

Equations

Std.instInhabitedFormat = { default := Lean.Format.nil }

source

def Std.Format.isEmpty :

Lean.Format → Bool

Check whether the given format contains no characters.

Equations

Lean.Format.nil.isEmpty = true
Lean.Format.line.isEmpty = false
(Lean.Format.align force).isEmpty = true
(Std.Format.text msg).isEmpty = (msg == "")
(Lean.Format.nest indent f).isEmpty = f.isEmpty
(f₁.append f₂).isEmpty = (f₁.isEmpty && f₂.isEmpty)
(f.group behavior).isEmpty = f.isEmpty
(Lean.Format.tag a f).isEmpty = f.isEmpty

source

def Std.Format.fill (f : Lean.Format) :

Lean.Format

Alias for a group with FlattenBehavior set to fill.

Equations

f.fill = f.group Std.Format.FlattenBehavior.fill

source

instance Std.Format.instAppend :

Append Lean.Format

Equations

Std.Format.instAppend = { append := Std.Format.append }

source

instance Std.Format.instCoeString :

Coe String Lean.Format

Equations

Std.Format.instCoeString = { coe := Std.Format.text }

source

def Std.Format.join (xs : List Lean.Format) :

Lean.Format

Equations

Lean.Format.join xs = List.foldl (fun (x1 x2 : Lean.Format) => x1 ++ x2) (Std.Format.text "") xs

source

def Std.Format.isNil :

Lean.Format → Bool

Equations

Lean.Format.nil.isNil = true
x.isNil = false

source

instance Std.Format.instInhabitedSpaceResult :

Inhabited Std.Format.SpaceResult

Equations

Std.Format.instInhabitedSpaceResult = { default := { foundLine := default, foundFlattenedHardLine := default, space := default } }

source

class Std.Format.MonadPrettyFormat (m : Type → Type) :

Type

A monad in which we can pretty-print Format objects.

pushOutput : String → m Unit
pushNewline : Nat → m Unit
currColumn : m Nat
startTag : Nat → m Unit
Start a scope tagged with n.
endTags : Nat → m Unit
Exit the scope of n-many opened tags.

Instances

source

def Std.Format.prettyM {m : Type → Type} (f : Lean.Format) (w : Nat) (indent : optParam Nat 0) [Monad m] [Std.Format.MonadPrettyFormat m] :

m Unit

Render the given f : Format with a line width of w. indent is the starting amount to indent each line by.

Equations

f.prettyM w indent = Std.Format.be w [{ flatten := false, flb := Std.Format.FlattenBehavior.allOrNone, items := [{ f := f, indent := ↑indent, activeTags := 0 }] }]

source

@[inline]

def Std.Format.bracket (l : String) (f : Lean.Format) (r : String) :

Lean.Format

Create a format l ++ f ++ r with a flatten group. FlattenBehaviour is allOrNone; for fill use bracketFill.

Equations

Lean.Format.bracket l f r = (Lean.Format.nest (↑l.length) (Std.Format.text l ++ f ++ Std.Format.text r)).group

source

@[inline]

def Std.Format.paren (f : Lean.Format) :

Lean.Format

Creates the format "(" ++ f ++ ")" with a flattening group.

Equations

f.paren = Lean.Format.bracket "(" f ")"

source

@[inline]

def Std.Format.sbracket (f : Lean.Format) :

Lean.Format

Creates the format "[" ++ f ++ "]" with a flattening group.

Equations

f.sbracket = Lean.Format.bracket "[" f "]"

source

@[inline]

def Std.Format.bracketFill (l : String) (f : Lean.Format) (r : String) :

Lean.Format

Same as bracket except uses the fill flattening behaviour.

Equations

Std.Format.bracketFill l f r = (Lean.Format.nest (↑l.length) (Std.Format.text l ++ f ++ Std.Format.text r)).fill

source

def Std.Format.defIndent :

Nat

Default indentation.

Equations

Std.Format.defIndent = 2

source

def Std.Format.defUnicode :

Bool

Equations

Std.Format.defUnicode = true

source

def Std.Format.defWidth :

Nat

Default width of the targeted output pane.

Equations

Std.Format.defWidth = 120

source

def Std.Format.nestD (f : Lean.Format) :

Lean.Format

Nest with the default indentation amount.

Equations

f.nestD = Lean.Format.nest (↑Std.Format.defIndent) f

source

def Std.Format.indentD (f : Lean.Format) :

Lean.Format

Insert a newline and then f, all nested by the default indent amount.

Equations

f.indentD = (Lean.Format.line ++ f).nestD

source

instance Std.Format.instMonadPrettyFormatStateMState :

Std.Format.MonadPrettyFormat (StateM Std.Format.State)

Equations

One or more equations did not get rendered due to their size.

source

@[export lean_format_pretty]

def Std.Format.pretty (f : Lean.Format) (width : optParam Nat Std.Format.defWidth) (indent : optParam Nat 0) (column : optParam Nat 0) :

String

Renders a Format to a string.

width: the total width
indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)
column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)

Equations