- start : String.Pos
- stop : String.Pos
A position range inside a string. This type is mostly in combination with syntax trees,
as there might not be a single underlying string in this case that could be used for a Substring
.
Instances For
Instances For
Instances For
Syntax AST #
- mk: ∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax), Lean.IsNode (Lean.Syntax.node info kind args)
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Set 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.
The Syntax
argument is the output produced by the parser for source
.
This function "fixes" the source.leading
field.
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.
Instances For
Split an ident
into its dot-separated components while preserving source info.
Macro scopes are first erased. For example, `foo.bla.boo._@._hyg.4
↦ [`foo, `bla, `boo]
.
If nFields
is set, we take that many fields from the end and keep the remaining components
as one name. For example, `foo.bla.boo
with (nFields := 1)
↦ [`foo.bla, `boo]
.
Instances For
for _ in stx.topDown
iterates through each node and leaf in stx
top-down, left-to-right.
If firstChoiceOnly
is true
, only visit the first argument of each choice node.
Instances For
Instances For
Instances For
- cur : Lean.Syntax
- parents : Array 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 cur
is Syntax.missing
.
If the Traverser
is used linearly, updates are linear in the Syntax
object as well.
Instances For
Instances For
Advance to the idx
-th child of the current node.
Instances For
Advance to the parent of the current node, if any.
Instances For
Advance to the left sibling of the current node, if any.
Instances For
Advance to the right sibling of the current node, if any.
Instances For
- st : MonadState Lean.Syntax.Traverser m
Monad class that gives read/write access to a Traverser
.
Instances
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see mkAntiquot
).
Instances For
Instances For
Instances For
Instances For
List of Syntax
nodes in which each succeeding element is the parent of
the current. The associated index is the index of the preceding element in the
list of children of the current element.
Instances For
Return stack of syntax nodes satisfying visit
, starting with such a node that also fulfills accept
(default "is leaf"), and ending with the root.
Instances For
Compare the SyntaxNodeKind
s in pattern
to those of the Syntax
elements in stack
. Return false
if stack
is shorter than pattern
.