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

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

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.

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.