The formatter turns a Syntax tree into a Format object, inserting both mandatory whitespace (to separate adjacent tokens) as well as "pretty" optional whitespace.

The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree, driven by parser-specific handlers registered via attributes. The traversal is right-to-left so that when emitting a token, we already know the text following it and can decide whether or not whitespace between the two is necessary.

structure Lean.PrettyPrinter.Formatter.Context : Type

• options : Options
• table : Parser.TokenTable

structure Lean.PrettyPrinter.Formatter.State : Type

• stxTrav : Syntax.Traverser
• leadWord : String

  Textual content of stack up to the first whitespace (not enclosed in an escaped ident). We assume that the textual content of stack is modified only by push and pushWhitespace, so leadWord is adjusted there accordingly.

• leadWordIdent : Bool

  When the leadWord is nonempty, whether it is an identifier. Identifiers get space inserted between them.

• isUngrouped : Bool

  Whether the generated format begins with the result of an ungrouped category formatter.

• mustBeGrouped : Bool

  Whether the resulting format must be grouped when used in a category formatter. If the flag is set to false, then categoryParser omits the fill+nest operation.

• stack : Array Format

  Stack of generated Format objects, analogous to the Syntax stack in the parser. Note, however, that the stack is reversed because of the right-to-left traversal.

@[reducible, inline]

abbrev Lean.PrettyPrinter.FormatterM (α : Type) : Type

Equations

• Lean.PrettyPrinter.FormatterM = ReaderT Lean.PrettyPrinter.Formatter.Context (StateRefT' IO.RealWorld Lean.PrettyPrinter.Formatter.State Lean.CoreM)

@[inline]

def Lean.PrettyPrinter.FormatterM.orElse {α : Type} (p₁ : FormatterM α) (p₂ : Unit → FormatterM α) : FormatterM α

Equations

• p₁.orElse p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun (x : Lean.Exception) => do set s p₂ ()

instance Lean.PrettyPrinter.instOrElseFormatterM {α : Type} : OrElse (FormatterM α)

Equations

• Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter : Type

Equations

• Lean.PrettyPrinter.Formatter = Lean.PrettyPrinter.FormatterM Unit

opaque Lean.PrettyPrinter.formatterAttribute : KeyedDeclsAttribute Formatter

Registers a formatter for a parser.

@[formatter k] registers a declaration of type Lean.PrettyPrinter.Formatter to be used for formatting syntax of kind k.

opaque Lean.PrettyPrinter.combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute

Registers a formatter for a parser combinator.

@[combinator_formatter c] registers a declaration of type Lean.PrettyPrinter.Formatter for the Parser declaration c. Note that, unlike with @[formatter], this is not a node kind since combinators usually do not introduce their own node kinds. The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of c, where Parser is replaced with Formatter in the parameter types.

def Lean.PrettyPrinter.Formatter.throwBacktrack {α : Type} : FormatterM α

Equations

• Lean.PrettyPrinter.Formatter.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)

instance Lean.PrettyPrinter.Formatter.instMonadTraverserFormatterM : Syntax.MonadTraverser FormatterM

Equations

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

def Lean.PrettyPrinter.Formatter.getStack : FormatterM (Array Format)

Equations

• Lean.PrettyPrinter.Formatter.getStack = do let st ← get pure st.stack

def Lean.PrettyPrinter.Formatter.getStackSize : FormatterM Nat

Equations

• Lean.PrettyPrinter.Formatter.getStackSize = do let stack ← Lean.PrettyPrinter.Formatter.getStack pure stack.size

def Lean.PrettyPrinter.Formatter.setStack (stack : Array Format) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.push (f : Format) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.resetLeadWord : FormatterM Unit

Resets the state associated with the lead word, inhibiting any automatic whitespace insertion between tokens.

Equations

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

def Lean.PrettyPrinter.Formatter.pushWhitespace (f : Format) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.pushLine : FormatterM Unit

Equations

• Lean.PrettyPrinter.Formatter.pushLine = Lean.PrettyPrinter.Formatter.pushWhitespace Std.Format.line

def Lean.PrettyPrinter.Formatter.pushAlign (force : Bool) : FormatterM Unit

Equations

• Lean.PrettyPrinter.Formatter.pushAlign force = Lean.PrettyPrinter.Formatter.pushWhitespace (Std.Format.align force)

def Lean.PrettyPrinter.Formatter.visitArgs (x : FormatterM Unit) : FormatterM Unit

Execute x at the right-most child of the current node, if any, then advance to the left. Runs x even if there are no children, in which case the current syntax node will be .missing.

Equations

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

def Lean.PrettyPrinter.Formatter.fold (fn : Array Format → Format) (x : FormatterM Unit) : FormatterM Unit

Execute x, pass array of generated Format objects to fn, and push result.

Equations

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

def Lean.PrettyPrinter.Formatter.concat (x : FormatterM Unit) : FormatterM Unit

Execute x and concatenate generated Format objects.

Equations

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

def Lean.PrettyPrinter.Formatter.indent (x : Formatter) (indent : Option Int := none) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.fill (x : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.group (x : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter

If pos? has a position, run x and tag its results with that position, if they are not already tagged. Otherwise just run x.

Equations

• One or more equations did not get rendered due to their size.
• Lean.PrettyPrinter.Formatter.withMaybeTag pos? x = x

partial def Lean.PrettyPrinter.Formatter.orelse.formatter (p1 p2 : Formatter) : Formatter

def Lean.PrettyPrinter.Formatter.recover.formatter (fmt : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.recover.formatter fmt = fmt

def Lean.PrettyPrinter.Formatter.recover'.formatter (fmt : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.recover'.formatter fmt = fmt

@[extern lean_mk_antiquot_formatter]

opaque Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' (name : String) (kind : SyntaxNodeKind) (anonymous : Bool := true) (isPseudoKind : Bool := false) : Formatter

@[extern lean_pretty_printer_formatter_interpret_parser_descr]

opaque Lean.PrettyPrinter.Formatter.interpretParserDescr' : ParserDescr → CoreM Formatter

def Lean.PrettyPrinter.Formatter.getExprPos? : Syntax → Option String.Pos

Equations

• Lean.PrettyPrinter.Formatter.getExprPos? (Lean.Syntax.node info kind args) = Lean.PrettyPrinter.Formatter.SourceInfo.getExprPos?✝ info
• Lean.PrettyPrinter.Formatter.getExprPos? (Lean.Syntax.atom info val) = Lean.PrettyPrinter.Formatter.SourceInfo.getExprPos?✝ info
• Lean.PrettyPrinter.Formatter.getExprPos? (Lean.Syntax.ident info rawVal val preresolved) = Lean.PrettyPrinter.Formatter.SourceInfo.getExprPos?✝ info
• Lean.PrettyPrinter.Formatter.getExprPos? Lean.Syntax.missing = none

unsafe def Lean.PrettyPrinter.Formatter.formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter

Equations

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

@[implemented_by Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]

opaque Lean.PrettyPrinter.Formatter.formatterForKind (k : SyntaxNodeKind) : Formatter

def Lean.PrettyPrinter.Formatter.withAntiquot.formatter (antiP p : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.withAntiquot.formatter antiP p = Lean.PrettyPrinter.Formatter.orelse.formatter antiP p

def Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter : SyntaxNodeKind → (p suffix : Formatter) → Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.tokenWithAntiquot.formatter (p : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryFormatterCore (cat : Name) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryParser.formatter (cat : Name) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.categoryFormatter (cat : Name) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.categoryFormatter cat = (Lean.PrettyPrinter.Formatter.categoryFormatterCore cat).indent.fill

def Lean.PrettyPrinter.Formatter.parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.error.formatter (_msg : String) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.error.formatter _msg = pure ()

def Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.errorAtSavedPos.formatter _msg _delta = pure ()

def Lean.PrettyPrinter.Formatter.lookahead.formatter : Formatter → Formatter

Equations

• Lean.PrettyPrinter.Formatter.lookahead.formatter x✝ = pure ()

def Lean.PrettyPrinter.Formatter.notFollowedBy.formatter : Formatter → Formatter

Equations

• Lean.PrettyPrinter.Formatter.notFollowedBy.formatter x✝ = pure ()

def Lean.PrettyPrinter.Formatter.andthen.formatter (p1 p2 : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = p2 *> p1

def Lean.PrettyPrinter.Formatter.checkKind (k : SyntaxNodeKind) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.node.formatter k p = do Lean.PrettyPrinter.Formatter.checkKind k Lean.PrettyPrinter.Formatter.visitArgs p

def Lean.PrettyPrinter.Formatter.withFn.formatter : (Parser.ParserFn → Parser.ParserFn) → (p : Formatter) → Formatter

Equations

• Lean.PrettyPrinter.Formatter.withFn.formatter x✝ p = p

def Lean.PrettyPrinter.Formatter.trailingNode.formatter (k : SyntaxNodeKind) : Nat → Nat → (p : Formatter) → Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.parseToken (s : String) : FormatterM Parser.ParserState

Equations

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

def Lean.PrettyPrinter.Formatter.pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter (sym : String) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter (sym : String) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.rawCh.formatter (ch : Char) (trailingWs : Bool := false) : FormatterM Unit

Equations

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

def Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.identNoAntiquot.formatter : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.identEq.formatter (_id : Name) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.identEq.formatter _id = Lean.PrettyPrinter.Formatter.rawIdentNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.visitAtom (k : SyntaxNodeKind) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.charLitKind

def Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.strLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.strLitKind

def Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.nameLitKind

def Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.numLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.numLitKind

def Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.scientificLitKind

def Lean.PrettyPrinter.Formatter.fieldIdx.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.fieldIdx.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.fieldIdxKind

def Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter (p : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter (p : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.many1NoAntiquot.formatter p = Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p

def Lean.PrettyPrinter.Formatter.optionalNoAntiquot.formatter (p : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.many1Unbox.formatter (p : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter

Equations

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

def Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter (p pSep : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter = Lean.PrettyPrinter.Formatter.sepByNoAntiquot.formatter

def Lean.PrettyPrinter.Formatter.withoutInfo.formatter (p : Formatter) : Formatter

Equations

• Lean.PrettyPrinter.Formatter.withoutInfo.formatter p = p

def Lean.PrettyPrinter.Formatter.checkWsBefore.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkWsBefore.formatter = do let st ← get if (st.leadWord != "") = true then Lean.PrettyPrinter.Formatter.pushLine else pure PUnit.unit

def Lean.PrettyPrinter.Formatter.checkPrec.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.setLhsPrec.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.setLhsPrec.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkStackTop.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkStackTop.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter = Lean.PrettyPrinter.Formatter.resetLeadWord

def Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkTailWs.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkTailWs.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColEq.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColEq.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGe.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColGe.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkColGt.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkColGt.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkLineEq.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkLineEq.formatter = pure ()

def Lean.PrettyPrinter.Formatter.eoi.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.eoi.formatter = pure ()

def Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter = pure ()

def Lean.PrettyPrinter.Formatter.skip.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.skip.formatter = pure ()

def Lean.PrettyPrinter.Formatter.pushNone.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.pushNone.formatter = Lean.Syntax.MonadTraverser.goLeft

def Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter : Formatter

Equations

• Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter = Lean.Syntax.MonadTraverser.goLeft

def Lean.PrettyPrinter.Formatter.interpolatedStr.formatter (p : Formatter) : Formatter

Equations

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

@[macro_inline]

def Lean.PrettyPrinter.Formatter.ite : {x : Type} → (c : Prop) → [Decidable c] → (t e : Formatter) → Formatter

Equations

• Lean.PrettyPrinter.Formatter.ite c t e = if c then t else e

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type

Equations

• Lean.PrettyPrinter.Formatter.FormatterAliasValue = Lean.Parser.AliasValue Lean.PrettyPrinter.Formatter

opaque Lean.PrettyPrinter.Formatter.formatterAliasesRef : IO.Ref (NameMap FormatterAliasValue)

def Lean.PrettyPrinter.Formatter.registerAlias (aliasName : Name) (v : FormatterAliasValue) : IO Unit

Equations

• Lean.PrettyPrinter.Formatter.registerAlias aliasName v = Lean.Parser.registerAliasCore Lean.PrettyPrinter.Formatter.formatterAliasesRef aliasName v

instance Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue : Coe Formatter FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue = { coe := Lean.Parser.AliasValue.const }

instance Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue : Coe (Formatter → Formatter) FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.unary }

instance Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue : Coe (Formatter → Formatter → Formatter) FormatterAliasValue

Equations

• Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.binary }

opaque Lean.PrettyPrinter.pp.oneline : Lean.Option Bool

The OneLine.pretty function takes the first line of a Format while preserving tags.

structure Lean.PrettyPrinter.OneLine.State : Type

• line : Format
• column : Nat
• tags : List (Nat × Format)

@[reducible, inline]

abbrev Lean.PrettyPrinter.OneLine.M (α : Type) : Type

We use EStateM to be able to abort pretty printing once we get to the end of a line.

Equations

• Lean.PrettyPrinter.OneLine.M = EStateM Unit Lean.PrettyPrinter.OneLine.State

def Lean.PrettyPrinter.OneLine.continuation : String

Equations

• Lean.PrettyPrinter.OneLine.continuation = " [...]"

instance Lean.PrettyPrinter.OneLine.instMonadPrettyFormatM : Std.Format.MonadPrettyFormat M

Equations

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

def Lean.PrettyPrinter.OneLine.pretty (f : Format) (width : Nat) : Format

Pretty prints f and creates a new Format of its first line. Preserves tags.

Equations

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

def Lean.PrettyPrinter.format (formatter : Formatter) (stx : Syntax) : CoreM Format

Equations

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

def Lean.PrettyPrinter.formatCategory (cat : Name) (stx : Syntax) : CoreM Format

Equations

• Lean.PrettyPrinter.formatCategory cat = Lean.PrettyPrinter.format (Lean.PrettyPrinter.Formatter.categoryFormatter cat)

def Lean.PrettyPrinter.formatTerm (stx : Syntax) : CoreM Format

Equations

• Lean.PrettyPrinter.formatTerm = Lean.PrettyPrinter.formatCategory `term

def Lean.PrettyPrinter.formatTactic (stx : Syntax) : CoreM Format

Equations

• Lean.PrettyPrinter.formatTactic = Lean.PrettyPrinter.formatCategory `tactic

def Lean.PrettyPrinter.formatCommand (stx : Syntax) : CoreM Format

Equations

• Lean.PrettyPrinter.formatCommand = Lean.PrettyPrinter.formatCategory `command