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 pushText and pushLine, 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

@[inline]

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

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

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter : Type

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

opaque Lean.PrettyPrinter.formatterAttribute : KeyedDeclsAttribute Formatter

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

opaque Lean.PrettyPrinter.combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute

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

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

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

def Lean.PrettyPrinter.Formatter.getStackSize : FormatterM Nat

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

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

def Lean.PrettyPrinter.Formatter.pushLine : FormatterM Unit

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

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.

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.

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

Execute x and concatenate generated Format objects.

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

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

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

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.

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

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

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

@[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

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

@[implemented_by Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[macro_inline]

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

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type

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

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

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

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

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

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

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

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

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

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

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