def
Lean.Elab.getDeclarationRange
{m : Type → Type}
[Monad m]
[Lean.MonadFileMap m]
(stx : Lean.Syntax)
:
Instances For
For most builtin declarations, the selection range is just its name, which is stored in the second position. Example:
"def " >> declId >> optDeclSig >> declVal
If the declaration name is absent, we use the keyword instead.
This function converts the given Syntax
into one that represents its "selection range".
Instances For
def
Lean.Elab.addDeclarationRanges
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadFileMap m]
(declName : Lake.Name)
(stx : Lean.Syntax)
:
m Unit
Store the range
and selectionRange
for declName
where stx
is the whole syntax object decribing declName
.
This method is for the builtin declarations only.
User-defined commands should use Lean.addDeclarationRanges
to store this information for their commands.
Instances For
def
Lean.Elab.addAuxDeclarationRanges
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
[Lean.MonadFileMap m]
(declName : Lake.Name)
(stx : Lean.Syntax)
(header : Lean.Syntax)
:
m Unit
Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc.