Syntax AST #
SourceInfo.leading according to the trailing stop of the preceding token.
The result is a round-tripping syntax tree IF, in the input syntax tree,
- all leading stops, atom contents, and trailing starts are correct
- trailing stops are between the trailing start and the next leading stop.
Remark: after parsing, all
SourceInfo.leading fields are empty.
Syntax argument is the output produced by the parser for
This function "fixes" the
Additionally, we try to choose "nicer" splits between leading and trailing stops according to some heuristics so that e.g. comments are associated to the (intuitively) correct token.
Note that the
SourceInfo.trailing fields must be correct.
The implementation of this Function relies on this property.
ident into its dot-separated components while preserving source info.
Macro scopes are first erased. For example,
[`foo, `bla, `boo].
nFields is set, we take that many fields from the end and keep the remaining components
as one name. For example,
(nFields := 1) ↦
- cur : Lean.Syntax
Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
Indices are allowed to be out-of-bound, in which case
Traverser is used linearly, updates are linear in the
Syntax object as well.
Return stack of syntax nodes satisfying
visit, starting with such a node that also fulfills
accept (default "is leaf"), and ending with the root.