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 : FlattenBehavior
• fill : FlattenBehavior

instance Std.Format.instInhabitedFlattenBehavior : Inhabited FlattenBehavior

instance Std.Format.instBEqFlattenBehavior : BEq FlattenBehavior

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 : Format

  The empty format.

• line : Format

  A position where a newline may be inserted if the current group does not fit within the allotted column width.

• align (force : Bool) : 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 → Format

  A node containing a plain string.

• nest (indent : Int) : Format → 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 : Format → Format → Format

  Concatenation of two Formats.

• group : Format → (behavior : optParam FlattenBehavior FlattenBehavior.allOrNone) → Format

  Creates a new flattening group for the given inner format.

• tag : Nat → Format → Format

  Used for associating auxiliary information (e.g. Exprs) with Format objects.

instance Std.instInhabitedFormat : Inhabited Format

def Std.Format.isEmpty : Format → Bool

Check whether the given format contains no characters.

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

Alias for a group with FlattenBehavior set to fill.

instance Std.Format.instAppend : Append Format

instance Std.Format.instCoeString : Coe String Format

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

def Std.Format.isNil : Format → Bool

instance Std.Format.instInhabitedSpaceResult : Inhabited Std.Format.SpaceResult✝

inductive Std.Format.FlattenAllowability : Type

A directive indicating whether a given work group is able to be flattened.

• allow indicates that the group is allowed to be flattened; its argument is true if there is sufficient space for it to be flattened (and so it should be), or false if not.
• disallow means that this group should not be flattened irrespective of space concerns. This is used at levels of a Format outside of any flattening groups. It is necessary to track this so that, after a hard line break, we know whether to try to flatten the next line.

• allow (fits : Bool) : FlattenAllowability
• disallow : FlattenAllowability

instance Std.Format.instBEqFlattenAllowability : BEq FlattenAllowability

def Std.Format.FlattenAllowability.shouldFlatten : FlattenAllowability → Bool

Whether the given directive indicates that flattening should occur.

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

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

• pushOutput (s : String) : m Unit
• pushNewline (indent : 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.

def Std.Format.prettyM {m : Type → Type} (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [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.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

Same as bracket except uses the fill flattening behaviour.

def Std.Format.defIndent : Nat

Default indentation.

def Std.Format.defUnicode : Bool

def Std.Format.defWidth : Nat

Default width of the targeted output pane.

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

Nest with the default indentation amount.

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

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

instance Std.Format.instMonadPrettyFormatStateMState : MonadPrettyFormat (StateM Std.Format.State✝)

@[export lean_format_pretty]

def Std.Format.pretty (f : Format) (width : Nat := defWidth) (indent column : 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)

class Std.ToFormat (α : Type u) : Type u

Class for converting a given type α to a Format object for pretty-printing. See also Repr, which also outputs a Format object.

• format : α → Format

instance Std.instToFormatFormat : ToFormat Format

instance Std.instToFormatString : ToFormat String

def Std.Format.joinSep {α : Type u} [ToFormat α] : List α → Format → Format

Intersperse the given list (each item printed with format) with the given sep format.

def Std.Format.prefixJoin {α : Type u} [ToFormat α] (pre : Format) : List α → Format

Format each item in items and prepend prefix pre.

def Std.Format.joinSuffix {α : Type u} [ToFormat α] : List α → Format → Format

Format each item in items and append suffix.