source
def Lean.Elab.getDeclarationRange? {m : Type → Type} [Monad m] [MonadFileMap m] (stx : Syntax) :
m (Option DeclarationRange)
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.getDeclarationSelectionRef (stx : Syntax) :
Syntax

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".

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.addDeclarationRangesFromSyntax {m : Type → Type} [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (rangeStx : Syntax) (selectionRangeStx : Syntax := Syntax.missing) :
m Unit

Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range, nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of `rangeStx`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.addDeclarationRangesForBuiltin {m : Type → Type} [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (modsStx : TSyntax `Lean.Parser.Command.declModifiers) (declStx : Syntax) :
m Unit

Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and `cmdStx` the remaining part of the syntax tree for `declName`.

This method is for the builtin declarations only. User-defined commands should use `Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information for their commands.

Equations

- One or more equations did not get rendered due to their size.

Instances For