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

  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 Lean.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₁ : Lean.PrettyPrinter.FormatterM α) (p₂ : Unit → Lean.PrettyPrinter.FormatterM α) : Lean.PrettyPrinter.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 (Lean.PrettyPrinter.FormatterM α)

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter : Type

Equations

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

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)

Equations

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

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

Equations

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

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

Equations

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

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. 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 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.

Equations

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

def Lean.PrettyPrinter.Formatter.concat (x : Lean.PrettyPrinter.FormatterM Unit) : Lean.PrettyPrinter.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 : Lean.PrettyPrinter.Formatter) (indent : Option Int := none) : Lean.PrettyPrinter.Formatter

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

Equations

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

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

Equations

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

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.

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 : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

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

Equations

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

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

Equations

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

@[extern lean_mk_antiquot_formatter]

opaque Lean.PrettyPrinter.Formatter.mkAntiquot.formatter' (name : String) (kind : Lean.SyntaxNodeKind) (anonymous : Bool := true) (isPseudoKind : 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 p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Equations

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

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

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

Equations

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

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

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

def Lean.PrettyPrinter.Formatter.categoryFormatter (cat : Lean.Name) : Lean.PrettyPrinter.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) : Lean.PrettyPrinter.Formatter

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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 : (Lean.Parser.ParserFn → Lean.Parser.ParserFn) → (p : Lean.PrettyPrinter.Formatter) → Lean.PrettyPrinter.Formatter

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 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 : Lean.Name) : Lean.PrettyPrinter.Formatter

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

• Lean.PrettyPrinter.Formatter.sepBy1NoAntiquot.formatter = Lean.PrettyPrinter.Formatter.sepByNoAntiquot.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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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] → (t e : Lean.PrettyPrinter.Formatter) → Lean.PrettyPrinter.Formatter

Equations

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

@[reducible, inline]

abbrev Lean.PrettyPrinter.Formatter.FormatterAliasValue : Type

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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 : Lean.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

Equations

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