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 : Lean.Options
• table : Lean.Parser.TokenTable

structure Lean.PrettyPrinter.Formatter.State : Type

• stxTrav : Lean.Syntax.Traverser
• leadWord : String
• isUngrouped : Bool
• mustBeGrouped : Bool
• stack : Array Lean.Format

@[inline, reducible]

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

@[inline]

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

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

@[inline, reducible]

abbrev Lean.PrettyPrinter.Formatter : Type

unsafe def Lean.PrettyPrinter.mkFormatterAttribute : IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter)

opaque Lean.PrettyPrinter.formatterAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Formatter

unsafe def Lean.PrettyPrinter.mkCombinatorFormatterAttribute : IO Lean.ParserCompiler.CombinatorAttribute

opaque Lean.PrettyPrinter.combinatorFormatterAttribute : Lean.ParserCompiler.CombinatorAttribute

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

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

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

def Lean.PrettyPrinter.Formatter.getStackSize : Lean.PrettyPrinter.FormatterM Nat

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

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

def Lean.PrettyPrinter.Formatter.pushLine : Lean.PrettyPrinter.FormatterM Unit

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

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

Execute x at the right-most child of the current node, if any, then advance to the left.

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

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

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

Execute x and concatenate generated Format objects.

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

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

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

def Lean.PrettyPrinter.Formatter.withMaybeTag (pos? : Option String.Pos) (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.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.

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

@[extern lean_mk_antiquot_formatter]

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

@[extern lean_pretty_printer_formatter_interpret_parser_descr]

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

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

@[implemented_by Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]

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

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

def Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

def Lean.PrettyPrinter.Formatter.rawCh.formatter (ch : Char) : Lean.PrettyPrinter.Formatter

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[macro_inline]

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

@[inline, reducible]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type

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

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

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

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

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

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

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

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

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

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

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