Lean4
/-- If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers
for the names of the declarations whose syntax begins in position at least `pos`.
-/
def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos) : m (Array Syntax) := do
-- declarations from parallelism branches should not be interesting here, so use `local`
let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv)
let fm ← getFileMap
let mut nms := #[]
for (nm, rgs) in drs do
if pos ≤ fm.ofPosition rgs.range.pos then
let ofPos1 := fm.ofPosition rgs.selectionRange.pos
let ofPos2 := fm.ofPosition rgs.selectionRange.endPos
nms := nms.push (mkIdentFrom (.ofRange ⟨ofPos1, ofPos2⟩) nm)
return nms
