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
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Execute x at the right-most child of the current node, if any, then advance to the left.
Instances For
Execute x, pass array of generated Format objects to fn, and push result.
Instances For
Execute x and concatenate generated Format objects.
Instances For
Instances For
Instances For
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.