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 : Options
- table : Parser.TokenTable
Instances For
- 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 ofstack
is modified only bypush
andpushWhitespace
, soleadWord
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 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.
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
Instances For
Registers a formatter for a parser.
@[formatter k]
registers a declaration of type Lean.PrettyPrinter.Formatter
to be used for
formatting syntax of kind k
.
Registers a formatter for a parser combinator.
@[combinator_formatter c]
registers a declaration of type Lean.PrettyPrinter.Formatter
for the
Parser
declaration c
. Note that, unlike with @[formatter]
, this is not a node kind since
combinators usually do not introduce their own node kinds. The tagged declaration may optionally
accept parameters corresponding to (a prefix of) those of c
, where Parser
is replaced with
Formatter
in the parameter types.
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
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
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
Instances For
Equations
Instances For
Equations
- Lean.PrettyPrinter.Formatter.andthen.formatter p1 p2 = p2 *> p1
Instances For
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
- 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
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
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
The OneLine.pretty
function takes the first line of a Format
while preserving tags.
We use EStateM
to be able to abort pretty printing once we get to the end of a line.
Instances For
Equations
- Lean.PrettyPrinter.OneLine.continuation = " [...]"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Pretty prints f
and creates a new Format
of its first line. Preserves tags.
Equations
- One or more equations did not get rendered due to their size.