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.
- options : Lean.Options
- table : Lean.Parser.TokenTable
Instances For
- stxTrav : Lean.Syntax.Traverser
- leadWord : String
- isUngrouped : Bool
- mustBeGrouped : Bool
- stack : Array Lean.Format
Instances For
Equations
Instances For
Equations
- p₁.orElse p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun (x : Lean.Exception) => do set s p₂ ()
Instances For
Equations
- Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.PrettyPrinter.Formatter.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.PrettyPrinter.Formatter.getStack = do let st ← get pure st.stack
Instances For
Equations
- Lean.PrettyPrinter.Formatter.getStackSize = do let stack ← Lean.PrettyPrinter.Formatter.getStack pure stack.size
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
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.
Instances For
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.
Instances For
Execute x
and concatenate generated Format objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = SeqRight.seqRight p2 fun (x : Unit) => p1
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.PrettyPrinter.Formatter.manyNoAntiquot.formatter p = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Formatter.visitArgs (stx.getArgs.size.forM fun (x : Nat) => p)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Lean.PrettyPrinter.Formatter.checkWsBefore.formatter = do let st ← get if (st.leadWord != "") = true then Lean.PrettyPrinter.Formatter.pushLine else pure PUnit.unit
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.PrettyPrinter.Formatter.pushNone.formatter = Lean.Syntax.MonadTraverser.goLeft
Instances For
Equations
- Lean.PrettyPrinter.Formatter.hygieneInfoNoAntiquot.formatter = Lean.Syntax.MonadTraverser.goLeft
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.PrettyPrinter.Formatter.ite c t e = if c then t else e
Instances For
Equations
Instances For
Equations
Instances For
Equations
- Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue = { coe := Lean.Parser.AliasValue.const }
Equations
- Lean.PrettyPrinter.Formatter.instCoeForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.unary }
Equations
- Lean.PrettyPrinter.Formatter.instCoeForallForallFormatterAliasValue = { coe := Lean.Parser.AliasValue.binary }
Equations
- One or more equations did not get rendered due to their size.