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

def Lean.Elab.getDeclarationSelectionRef (stx : Lean.Syntax) : Lean.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.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.

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.