fix: jump to correct definition when names overlap (#3656)
Fixes #1170. This PR adds the module name to `RefIdent` in order to distinguish conflicting names from different files. This also fixes related issues in find-references or the call hierarchy feature. It also adds some docstrings and stylistically refactors a bunch of code.
This commit is contained in:
Marc Huisinga
GitHub
parent
795e332fb3
commit
78a72741c6
6 changed files with 360 additions and 182 deletions
|
|
@ -24,44 +24,50 @@ Identifier of a reference.
|
|||
-/
|
||||
inductive RefIdent where
|
||||
/-- Named identifier. These are used in all references that are globally available. -/
|
||||
| const : Name → RefIdent
|
||||
| const (moduleName : Name) (identName : Name) : RefIdent
|
||||
/-- Unnamed identifier. These are used for all local references. -/
|
||||
| fvar : FVarId → RefIdent
|
||||
| fvar (moduleName : Name) (id : FVarId) : RefIdent
|
||||
deriving BEq, Hashable, Inhabited
|
||||
|
||||
namespace RefIdent
|
||||
|
||||
/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
|
||||
def toString : RefIdent → String
|
||||
| RefIdent.const n => s!"c:{n}"
|
||||
| RefIdent.fvar id => s!"f:{id.name}"
|
||||
instance : ToJson FVarId where
|
||||
toJson id := toJson id.name
|
||||
|
||||
/--
|
||||
Converts the string representation of a reference identifier back to a reference identifier.
|
||||
The string representation must have been created by `RefIdent.toString`.
|
||||
-/
|
||||
def fromString (s : String) : Except String RefIdent := do
|
||||
let sPrefix := s.take 2
|
||||
let sName := s.drop 2
|
||||
-- See `FromJson Name`
|
||||
let name ← match sName with
|
||||
| "[anonymous]" => pure Name.anonymous
|
||||
| _ =>
|
||||
let n := sName.toName
|
||||
if n.isAnonymous then throw s!"expected a Name, got {sName}"
|
||||
else pure n
|
||||
match sPrefix with
|
||||
| "c:" => return RefIdent.const name
|
||||
| "f:" => return RefIdent.fvar <| FVarId.mk name
|
||||
| _ => throw "string must start with 'c:' or 'f:'"
|
||||
instance : FromJson FVarId where
|
||||
fromJson? s := return ⟨← fromJson? s⟩
|
||||
|
||||
/-- Shortened representation of `RefIdent` for more compact serialization. -/
|
||||
inductive RefIdentJsonRepr
|
||||
/-- Shortened representation of `RefIdent.const` for more compact serialization. -/
|
||||
| c (m n : Name)
|
||||
/-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/
|
||||
| f (m : Name) (i : FVarId)
|
||||
deriving FromJson, ToJson
|
||||
|
||||
/-- Converts `id` to its compact serialization representation. -/
|
||||
def toJsonRepr : (id : RefIdent) → RefIdentJsonRepr
|
||||
| const moduleName identName => .c moduleName identName
|
||||
| fvar moduleName id => .f moduleName id
|
||||
|
||||
/-- Converts `repr` to `RefIdent`. -/
|
||||
def fromJsonRepr : (repr : RefIdentJsonRepr) → RefIdent
|
||||
| .c m n => const m n
|
||||
| .f m i => fvar m i
|
||||
|
||||
/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/
|
||||
def fromJson? (s : Json) : Except String RefIdent :=
|
||||
return fromJsonRepr (← Lean.FromJson.fromJson? s)
|
||||
|
||||
/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/
|
||||
def toJson (id : RefIdent) : Json :=
|
||||
Lean.ToJson.toJson <| toJsonRepr id
|
||||
|
||||
instance : FromJson RefIdent where
|
||||
fromJson?
|
||||
| (s : String) => fromString s
|
||||
| j => Except.error s!"expected a String, got {j}"
|
||||
fromJson? := fromJson?
|
||||
|
||||
instance : ToJson RefIdent where
|
||||
toJson ident := toString ident
|
||||
toJson := toJson
|
||||
|
||||
end RefIdent
|
||||
|
||||
|
|
@ -147,13 +153,13 @@ instance : FromJson RefInfo where
|
|||
def ModuleRefs := HashMap RefIdent RefInfo
|
||||
|
||||
instance : ToJson ModuleRefs where
|
||||
toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
|
||||
toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
|
||||
|
||||
instance : FromJson ModuleRefs where
|
||||
fromJson? j := do
|
||||
let node ← j.getObj?
|
||||
node.foldM (init := HashMap.empty) fun m k v =>
|
||||
return m.insert (← RefIdent.fromString k) (← fromJson? v)
|
||||
return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
|
||||
|
||||
/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
|
||||
|
||||
|
|
|
|||
|
|
@ -188,9 +188,9 @@ def unusedVariables : Linter where
|
|||
|
||||
for (ident, info) in refs.toList do
|
||||
match ident with
|
||||
| .fvar id =>
|
||||
| .fvar _ id =>
|
||||
vars := vars.insert id info
|
||||
| .const _ =>
|
||||
| .const .. =>
|
||||
if let some definition := info.definition then
|
||||
if let some range := definition.stx.getRange? then
|
||||
constDecls := constDecls.insert range
|
||||
|
|
@ -241,7 +241,7 @@ def unusedVariables : Linter where
|
|||
continue
|
||||
|
||||
-- check if variable is used
|
||||
if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then
|
||||
if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar _ id => tacticFVarUses.contains id | _ => false) then
|
||||
continue
|
||||
|
||||
-- check linter options
|
||||
|
|
|
|||
|
|
@ -10,34 +10,62 @@ import Lean.Server.Utils
|
|||
|
||||
/-! # Representing collected and deduplicated definitions and usages -/
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
namespace Lean.Server
|
||||
open Lsp Lean.Elab Std
|
||||
|
||||
/--
|
||||
Global reference. Used by the language server to figure out which identifiers refer to which
|
||||
other identifiers across the whole project.
|
||||
-/
|
||||
structure Reference where
|
||||
/-- Identifier of this reference. -/
|
||||
ident : RefIdent
|
||||
/-- FVarIds that are logically identical to this reference -/
|
||||
/-- Identifiers that are logically identical to this reference. -/
|
||||
aliases : Array RefIdent := #[]
|
||||
/-- Range where this reference occurs. -/
|
||||
range : Lsp.Range
|
||||
/-- Syntax of this reference. -/
|
||||
stx : Syntax
|
||||
/-- `ContextInfo` at the point of elaboration of this reference. -/
|
||||
ci : ContextInfo
|
||||
/-- Additional `InfoTree` information for this reference. -/
|
||||
info : Info
|
||||
/-- Whether this reference declares `ident`. -/
|
||||
isBinder : Bool
|
||||
|
||||
/-- Definition and usages of an identifier within a single module. -/
|
||||
structure RefInfo where
|
||||
/--
|
||||
Definition `Reference` of the identifier.
|
||||
Is equal to `none` if e.g. the definition is outside of the module where this `RefInfo` is used.
|
||||
-/
|
||||
definition : Option Reference
|
||||
/-- All usage `Reference`s of the identifier in a single module. -/
|
||||
usages : Array Reference
|
||||
|
||||
namespace RefInfo
|
||||
|
||||
def empty : RefInfo := ⟨ none, #[] ⟩
|
||||
/-- No definition, no usages. -/
|
||||
def empty : RefInfo := ⟨none, #[]⟩
|
||||
|
||||
def addRef : RefInfo → Reference → RefInfo
|
||||
| i@{ definition := none, .. }, ref@{ isBinder := true, .. } =>
|
||||
/--
|
||||
Adds `ref` to `i`.
|
||||
If `i` has no `definition` and `ref` is a declaration, it becomes the `definition`.
|
||||
If `i` already has a `definition` and `ref` is also a declaration, it is not added to `i`.
|
||||
Otherwise, `ref` is added to `i.usages`.
|
||||
-/
|
||||
def addRef (i : RefInfo) (ref : Reference) : RefInfo :=
|
||||
match i, ref with
|
||||
| { definition := none, .. }, { isBinder := true, .. } =>
|
||||
{ i with definition := ref }
|
||||
| i@{ usages, .. }, ref@{ isBinder := false, .. } =>
|
||||
| { definition := some .., .. }, { isBinder := true, .. } =>
|
||||
i
|
||||
| { usages, .. }, { isBinder := false, .. } =>
|
||||
{ i with usages := usages.push ref }
|
||||
| i, _ => i
|
||||
|
||||
/-- Converts `i` to a JSON-serializable `Lsp.RefInfo`. -/
|
||||
def toLspRefInfo (i : RefInfo) : BaseIO Lsp.RefInfo := do
|
||||
let refToRefInfoLocation (ref : Reference) : BaseIO RefInfo.Location := do
|
||||
let parentDeclName? := ref.ci.parentDecl?
|
||||
|
|
@ -64,14 +92,17 @@ def toLspRefInfo (i : RefInfo) : BaseIO Lsp.RefInfo := do
|
|||
|
||||
end RefInfo
|
||||
|
||||
/-- All references from within a module for all identifiers used in a single module. -/
|
||||
def ModuleRefs := HashMap RefIdent RefInfo
|
||||
|
||||
namespace ModuleRefs
|
||||
|
||||
/-- Adds `ref` to the `RefInfo` corresponding to `ref.ident` in `self`. See `RefInfo.addRef`. -/
|
||||
def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs :=
|
||||
let refInfo := self.findD ref.ident RefInfo.empty
|
||||
self.insert ref.ident (refInfo.addRef ref)
|
||||
|
||||
/-- Converts `refs` to a JSON-serializable `Lsp.ModuleRefs`. -/
|
||||
def toLspModuleRefs (refs : ModuleRefs) : BaseIO Lsp.ModuleRefs := do
|
||||
let refs ← refs.toList.mapM fun (k, v) => do
|
||||
return (k, ← v.toLspRefInfo)
|
||||
|
|
@ -84,48 +115,64 @@ end Lean.Server
|
|||
namespace Lean.Lsp.RefInfo
|
||||
open Server
|
||||
|
||||
/-- No definition, no usages -/
|
||||
def empty : RefInfo := ⟨ none, #[] ⟩
|
||||
|
||||
def merge (a : RefInfo) (b : RefInfo) : RefInfo :=
|
||||
{
|
||||
definition? := b.definition?.orElse fun _ => a.definition?
|
||||
usages := a.usages.append b.usages
|
||||
}
|
||||
/-- Combines the `usages` of `a` and `b` and prefers the `definition?` of `b` over that of `a`. -/
|
||||
def merge (a : RefInfo) (b : RefInfo) : RefInfo where
|
||||
definition? := b.definition?.orElse fun _ => a.definition?
|
||||
usages := a.usages.append b.usages
|
||||
|
||||
def findRange? (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Option Range := do
|
||||
if let some ⟨range, _⟩ := self.definition? then
|
||||
if contains range pos then
|
||||
return range
|
||||
for ⟨range, _⟩ in self.usages do
|
||||
if contains range pos then
|
||||
return range
|
||||
/--
|
||||
Finds the first definition or usage in `self` where the `RefInfo.Location.range`
|
||||
contains the given `pos`. The `includeStop` parameter can be used to toggle between closed-interval
|
||||
and half-open-interval behavior for the range. Closed-interval behavior matches the expectation of
|
||||
VSCode when selecting an identifier at a cursor position (see #767).
|
||||
-/
|
||||
def findReferenceLocation?
|
||||
(self : RefInfo)
|
||||
(pos : Lsp.Position)
|
||||
(includeStop : Bool := false)
|
||||
: Option Location := do
|
||||
if let some loc := self.definition? then
|
||||
if contains loc.range pos then
|
||||
return loc
|
||||
for loc in self.usages do
|
||||
if contains loc.range pos then
|
||||
return loc
|
||||
none
|
||||
where
|
||||
contains (range : Lsp.Range) (pos : Lsp.Position) : Bool :=
|
||||
-- Note: includeStop is used here to toggle between closed-interval and half-open-interval
|
||||
-- behavior for the range. Closed-interval behavior matches the expectation of VSCode
|
||||
-- when selecting an identifier at a cursor position, see #767.
|
||||
range.start <= pos && (if includeStop then pos <= range.end else pos < range.end)
|
||||
|
||||
/-- Checks whether any of the ranges in `self.definition?` or `self.usages` contains `pos`. -/
|
||||
def contains (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Bool := Id.run do
|
||||
(self.findRange? pos includeStop).isSome
|
||||
(self.findReferenceLocation? pos includeStop).isSome
|
||||
|
||||
end Lean.Lsp.RefInfo
|
||||
|
||||
namespace Lean.Lsp.ModuleRefs
|
||||
open Server
|
||||
|
||||
def findAt (self : ModuleRefs) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do
|
||||
/--
|
||||
Find all identifiers in `self` with a reference in this module that contains `pos` in its range.
|
||||
-/
|
||||
def findAt
|
||||
(self : ModuleRefs)
|
||||
(pos : Lsp.Position)
|
||||
(includeStop := false)
|
||||
: Array RefIdent := Id.run do
|
||||
let mut result := #[]
|
||||
for (ident, info) in self.toList do
|
||||
for (ident, info) in self.toArray do
|
||||
if info.contains pos includeStop then
|
||||
result := result.push ident
|
||||
result
|
||||
|
||||
/-- Finds the first range in `self` that contains `pos`. -/
|
||||
def findRange? (self : ModuleRefs) (pos : Lsp.Position) (includeStop := false) : Option Range := do
|
||||
for (_, info) in self.toList do
|
||||
if let some range := info.findRange? pos includeStop then
|
||||
return range
|
||||
if let some loc := info.findReferenceLocation? pos includeStop then
|
||||
return loc.range
|
||||
none
|
||||
|
||||
end Lean.Lsp.ModuleRefs
|
||||
|
|
@ -137,13 +184,17 @@ open Elab
|
|||
|
||||
/-- Content of individual `.ilean` files -/
|
||||
structure Ilean where
|
||||
version : Nat := 2
|
||||
/-- Version number of the ilean format. -/
|
||||
version : Nat := 3
|
||||
/-- Name of the module that this ilean data has been collected for. -/
|
||||
module : Name
|
||||
/-- All references of this module. -/
|
||||
references : Lsp.ModuleRefs
|
||||
deriving FromJson, ToJson
|
||||
|
||||
namespace Ilean
|
||||
|
||||
/-- Reads and parses the .ilean file at `path`. -/
|
||||
def load (path : System.FilePath) : IO Ilean := do
|
||||
let content ← FS.readFile path
|
||||
match Json.parse content >>= fromJson? with
|
||||
|
|
@ -153,23 +204,33 @@ def load (path : System.FilePath) : IO Ilean := do
|
|||
end Ilean
|
||||
/-! # Collecting and deduplicating definitions and usages -/
|
||||
|
||||
def identOf : Info → Option (RefIdent × Bool)
|
||||
/--
|
||||
Determines the `RefIdent` for the `Info` `i` of an identifier in `module` and
|
||||
whether it is a declaration.
|
||||
-/
|
||||
def identOf (module : Name) (i : Info) : Option (RefIdent × Bool) :=
|
||||
match i with
|
||||
| Info.ofTermInfo ti => match ti.expr with
|
||||
| Expr.const n .. => some (RefIdent.const n, ti.isBinder)
|
||||
| Expr.fvar id .. => some (RefIdent.fvar id, ti.isBinder)
|
||||
| Expr.const n .. => some (RefIdent.const module n, ti.isBinder)
|
||||
| Expr.fvar id => some (RefIdent.fvar module id, ti.isBinder)
|
||||
| _ => none
|
||||
| Info.ofFieldInfo fi => some (RefIdent.const fi.projName, false)
|
||||
| Info.ofOptionInfo oi => some (RefIdent.const oi.declName, false)
|
||||
| Info.ofFieldInfo fi => some (RefIdent.const module fi.projName, false)
|
||||
| Info.ofOptionInfo oi => some (RefIdent.const module oi.declName, false)
|
||||
| _ => none
|
||||
|
||||
def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference := Id.run <| StateT.run' (s := #[]) do
|
||||
for tree in trees do
|
||||
tree.visitM' (postNode := fun ci info _ => do
|
||||
if let some (ident, isBinder) := identOf info then
|
||||
if let some range := info.range? then
|
||||
if info.stx.getHeadInfo matches .original .. then -- we are not interested in canonical syntax here
|
||||
modify (·.push { ident, range := range.toLspRange text, stx := info.stx, ci, info, isBinder }))
|
||||
get
|
||||
/-- Finds all references in `trees`. -/
|
||||
def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference :=
|
||||
Id.run <| StateT.run' (s := #[]) do
|
||||
for tree in trees do
|
||||
tree.visitM' (postNode := fun ci info _ => do
|
||||
let mod := ci.env.header.mainModule
|
||||
let some (ident, isBinder) := identOf mod info
|
||||
| return
|
||||
let some range := info.range?
|
||||
| return
|
||||
if info.stx.getHeadInfo matches .original .. then -- we are not interested in canonical syntax here
|
||||
modify (·.push { ident, range := range.toLspRange text, stx := info.stx, ci, info, isBinder }))
|
||||
get
|
||||
|
||||
/--
|
||||
There are several different identifiers that should be considered equal for the purpose of finding
|
||||
|
|
@ -228,10 +289,10 @@ where
|
|||
for id in «class» do
|
||||
bestRepresentative :=
|
||||
match bestRepresentative, id with
|
||||
| .fvar a, .fvar _ => .fvar a
|
||||
| .fvar _, .const b => .const b
|
||||
| .const a, .fvar _ => .const a
|
||||
| .const a, .const _ => .const a
|
||||
| .fvar ma a, .fvar .. => .fvar ma a
|
||||
| .fvar .., .const mb b => .const mb b
|
||||
| .const ma a, .fvar .. => .const ma a
|
||||
| .const ma a, .const .. => .const ma a
|
||||
|
||||
-- compress `idMap` so that all identifiers in a class point to the best representative
|
||||
for id in «class» do
|
||||
|
|
@ -253,9 +314,11 @@ where
|
|||
insertIdMap id baseId
|
||||
|
||||
-- apply `FVarAliasInfo`
|
||||
trees.forM (·.visitM' (postNode := fun _ info _ => do
|
||||
trees.forM (·.visitM' (postNode := fun ci info _ => do
|
||||
if let .ofFVarAliasInfo ai := info then
|
||||
insertIdMap (.fvar ai.id) (.fvar ai.baseId)))
|
||||
-- FVars can only be aliases of FVars of the same file / module
|
||||
let mod := ci.env.header.mainModule
|
||||
insertIdMap (.fvar mod ai.id) (.fvar mod ai.baseId)))
|
||||
|
||||
get
|
||||
|
||||
|
|
@ -267,6 +330,11 @@ where
|
|||
if baseId != id then
|
||||
modify (·.insert id baseId)
|
||||
|
||||
/--
|
||||
Groups `refs` by identifier and range s.t. references with the same identifier and range
|
||||
are added to the `aliases` of the representative of the group.
|
||||
Yields to separate groups for declaration and usages if `allowSimultaneousBinderUse` is set.
|
||||
-/
|
||||
def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := false) : Array Reference := Id.run do
|
||||
let mut refsByIdAndRange : HashMap (RefIdent × Option Bool × Lsp.Range) Reference := HashMap.empty
|
||||
for ref in refs do
|
||||
|
|
@ -279,6 +347,10 @@ def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := fals
|
|||
let dedupedRefs := refsByIdAndRange.fold (init := #[]) fun refs _ ref => refs.push ref
|
||||
return dedupedRefs.qsort (·.range < ·.range)
|
||||
|
||||
/--
|
||||
Finds all references in `trees` and deduplicates the result.
|
||||
See `dedupReferences` and `combineIdents`.
|
||||
-/
|
||||
def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool := true)
|
||||
(allowSimultaneousBinderUse := false) : ModuleRefs := Id.run do
|
||||
let mut refs :=
|
||||
|
|
@ -287,12 +359,13 @@ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool :
|
|||
findReferences text trees
|
||||
if !localVars then
|
||||
refs := refs.filter fun
|
||||
| { ident := RefIdent.fvar _, .. } => false
|
||||
| { ident := RefIdent.fvar .., .. } => false
|
||||
| _ => true
|
||||
refs.foldl (init := HashMap.empty) fun m ref => m.addRef ref
|
||||
|
||||
/-! # Collecting and maintaining reference info from different sources -/
|
||||
|
||||
/-- References from ilean files and current ilean information from file workers. -/
|
||||
structure References where
|
||||
/-- References loaded from ilean files -/
|
||||
ileans : HashMap Name (System.FilePath × Lsp.ModuleRefs)
|
||||
|
|
@ -301,17 +374,25 @@ structure References where
|
|||
|
||||
namespace References
|
||||
|
||||
/-- No ilean files, no information from workers. -/
|
||||
def empty : References := { ileans := HashMap.empty, workers := HashMap.empty }
|
||||
|
||||
/-- Adds the contents of an ilean file `ilean` at `path` to `self`. -/
|
||||
def addIlean (self : References) (path : System.FilePath) (ilean : Ilean) : References :=
|
||||
{ self with ileans := self.ileans.insert ilean.module (path, ilean.references) }
|
||||
|
||||
/-- Removes the ilean file data at `path` from `self`. -/
|
||||
def removeIlean (self : References) (path : System.FilePath) : References :=
|
||||
let namesToRemove := self.ileans.toList.filter (fun (_, p, _) => p == path)
|
||||
|>.map (fun (n, _, _) => n)
|
||||
namesToRemove.foldl (init := self) fun self name =>
|
||||
{ self with ileans := self.ileans.erase name }
|
||||
|
||||
/--
|
||||
Updates the worker references in `self` with the `refs` of the worker managing the module `name`.
|
||||
Replaces the current references with `refs` if `version` is newer than the current version managed
|
||||
in `refs` and otherwise merges the reference data if `version` is equal to the current version.
|
||||
-/
|
||||
def updateWorkerRefs (self : References) (name : Name) (version : Nat) (refs : Lsp.ModuleRefs) : References := Id.run do
|
||||
if let some (currVersion, _) := self.workers.find? name then
|
||||
if version > currVersion then
|
||||
|
|
@ -323,78 +404,118 @@ def updateWorkerRefs (self : References) (name : Name) (version : Nat) (refs : L
|
|||
return { self with workers := self.workers.insert name (version, merged) }
|
||||
return self
|
||||
|
||||
/--
|
||||
Replaces the worker references in `self` with the `refs` of the worker managing the module `name`
|
||||
if `version` is newer than the current version managed in `refs`.
|
||||
-/
|
||||
def finalizeWorkerRefs (self : References) (name : Name) (version : Nat) (refs : Lsp.ModuleRefs) : References := Id.run do
|
||||
if let some (currVersion, _) := self.workers.find? name then
|
||||
if version < currVersion then
|
||||
return self
|
||||
return { self with workers := self.workers.insert name (version, refs) }
|
||||
|
||||
/-- Erases all worker references in `self` for the worker managing `name`. -/
|
||||
def removeWorkerRefs (self : References) (name : Name) : References :=
|
||||
{ self with workers := self.workers.erase name }
|
||||
|
||||
/-- Yields a map from all modules to all of their references. -/
|
||||
def allRefs (self : References) : HashMap Name Lsp.ModuleRefs :=
|
||||
let ileanRefs := self.ileans.toList.foldl (init := HashMap.empty) fun m (name, _, refs) => m.insert name refs
|
||||
self.workers.toList.foldl (init := ileanRefs) fun m (name, _, refs) => m.insert name refs
|
||||
let ileanRefs := self.ileans.toArray.foldl (init := HashMap.empty) fun m (name, _, refs) => m.insert name refs
|
||||
self.workers.toArray.foldl (init := ileanRefs) fun m (name, _, refs) => m.insert name refs
|
||||
|
||||
/--
|
||||
Yields all references in `self` for `ident`, as well as the `DocumentUri` that each
|
||||
reference occurs in.
|
||||
-/
|
||||
def allRefsFor
|
||||
(self : References)
|
||||
(srcSearchPath : SearchPath)
|
||||
(ident : RefIdent)
|
||||
: IO (Array (DocumentUri × Lsp.RefInfo)) := do
|
||||
let refsToCheck := match ident with
|
||||
| RefIdent.const .. => self.allRefs.toArray
|
||||
| RefIdent.fvar identModule .. =>
|
||||
match self.allRefs.find? identModule with
|
||||
| none => #[]
|
||||
| some refs => #[(identModule, refs)]
|
||||
let mut result := #[]
|
||||
for (module, refs) in refsToCheck do
|
||||
let some info := refs.find? ident
|
||||
| continue
|
||||
let some path ← srcSearchPath.findModuleWithExt "lean" module
|
||||
| continue
|
||||
-- Resolve symlinks (such as `src` in the build dir) so that files are
|
||||
-- opened in the right folder
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
result := result.push (uri, info)
|
||||
return result
|
||||
|
||||
/-- Yields all references in `module` at `pos`. -/
|
||||
def findAt (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Array RefIdent := Id.run do
|
||||
if let some refs := self.allRefs.find? module then
|
||||
return refs.findAt pos includeStop
|
||||
#[]
|
||||
|
||||
/-- Yields the first reference in `module` at `pos`. -/
|
||||
def findRange? (self : References) (module : Name) (pos : Lsp.Position) (includeStop := false) : Option Range := do
|
||||
let refs ← self.allRefs.find? module
|
||||
refs.findRange? pos includeStop
|
||||
|
||||
/-- Location and parent declaration of a reference. -/
|
||||
structure DocumentRefInfo where
|
||||
/-- Location of the reference. -/
|
||||
location : Location
|
||||
/-- Parent declaration of the reference. -/
|
||||
parentInfo? : Option RefInfo.ParentDecl
|
||||
|
||||
def referringTo (self : References) (identModule : Name) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
(includeDefinition : Bool := true) : IO (Array DocumentRefInfo) := do
|
||||
let refsToCheck := match ident with
|
||||
| RefIdent.const _ => self.allRefs.toList
|
||||
| RefIdent.fvar _ => match self.allRefs.find? identModule with
|
||||
| none => []
|
||||
| some refs => [(identModule, refs)]
|
||||
/-- Yields locations and parent declaration for all references referring to `ident`. -/
|
||||
def referringTo
|
||||
(self : References)
|
||||
(srcSearchPath : SearchPath)
|
||||
(ident : RefIdent)
|
||||
(includeDefinition : Bool := true)
|
||||
: IO (Array DocumentRefInfo) := do
|
||||
let mut result := #[]
|
||||
for (module, refs) in refsToCheck do
|
||||
if let some info := refs.find? ident then
|
||||
if let some path ← srcSearchPath.findModuleWithExt "lean" module then
|
||||
-- Resolve symlinks (such as `src` in the build dir) so that files are
|
||||
-- opened in the right folder
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
if includeDefinition then
|
||||
if let some ⟨range, parentDeclInfo?⟩ := info.definition? then
|
||||
result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩
|
||||
for ⟨range, parentDeclInfo?⟩ in info.usages do
|
||||
result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩
|
||||
for (moduleUri, info) in ← self.allRefsFor srcSearchPath ident do
|
||||
if includeDefinition then
|
||||
if let some ⟨range, parentDeclInfo?⟩ := info.definition? then
|
||||
result := result.push ⟨⟨moduleUri, range⟩, parentDeclInfo?⟩
|
||||
for ⟨range, parentDeclInfo?⟩ in info.usages do
|
||||
result := result.push ⟨⟨moduleUri, range⟩, parentDeclInfo?⟩
|
||||
return result
|
||||
|
||||
def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
/-- Yields the definition location of `ident`. -/
|
||||
def definitionOf?
|
||||
(self : References)
|
||||
(ident : RefIdent)
|
||||
(srcSearchPath : SearchPath)
|
||||
: IO (Option DocumentRefInfo) := do
|
||||
for (module, refs) in self.allRefs.toList do
|
||||
if let some info := refs.find? ident then
|
||||
if let some ⟨definitionRange, definitionParentDeclInfo?⟩ := info.definition? then
|
||||
if let some path ← srcSearchPath.findModuleWithExt "lean" module then
|
||||
-- Resolve symlinks (such as `src` in the build dir) so that files are
|
||||
-- opened in the right folder
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
return some ⟨⟨uri, definitionRange⟩, definitionParentDeclInfo?⟩
|
||||
for (moduleUri, info) in ← self.allRefsFor srcSearchPath ident do
|
||||
let some ⟨definitionRange, definitionParentDeclInfo?⟩ := info.definition?
|
||||
| continue
|
||||
return some ⟨⟨moduleUri, definitionRange⟩, definitionParentDeclInfo?⟩
|
||||
return none
|
||||
|
||||
def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter : Name → Option α)
|
||||
(maxAmount? : Option Nat := none) : IO $ Array (α × Location) := do
|
||||
/-- Yields all definitions matching the given `filter`. -/
|
||||
def definitionsMatching
|
||||
(self : References)
|
||||
(srcSearchPath : SearchPath)
|
||||
(filter : Name → Option α)
|
||||
(maxAmount? : Option Nat := none) : IO $ Array (α × Location) := do
|
||||
let mut result := #[]
|
||||
for (module, refs) in self.allRefs.toList do
|
||||
if let some path ← srcSearchPath.findModuleWithExt "lean" module then
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
for (ident, info) in refs.toList do
|
||||
if let (RefIdent.const name, some ⟨definitionRange, _⟩) := (ident, info.definition?) then
|
||||
if let some a := filter name then
|
||||
result := result.push (a, ⟨uri, definitionRange⟩)
|
||||
if let some maxAmount := maxAmount? then
|
||||
if result.size >= maxAmount then
|
||||
return result
|
||||
let some path ← srcSearchPath.findModuleWithExt "lean" module
|
||||
| continue
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
for (ident, info) in refs.toList do
|
||||
let (RefIdent.const _ name, some ⟨definitionRange, _⟩) := (ident, info.definition?)
|
||||
| continue
|
||||
let some a := filter name
|
||||
| continue
|
||||
result := result.push (a, ⟨uri, definitionRange⟩)
|
||||
if let some maxAmount := maxAmount? then
|
||||
if result.size >= maxAmount then
|
||||
return result
|
||||
return result
|
||||
|
||||
end References
|
||||
|
|
|
|||
|
|
@ -14,17 +14,20 @@ import Lean.Server.InfoUtils
|
|||
|
||||
namespace IO
|
||||
|
||||
/-- Throws an `IO.userError`. -/
|
||||
def throwServerError (err : String) : IO α :=
|
||||
throw (userError err)
|
||||
|
||||
namespace FS.Stream
|
||||
|
||||
/-- Chains two streams by creating a new stream s.t. writing to it
|
||||
/--
|
||||
Chains two streams by creating a new stream s.t. writing to it
|
||||
just writes to `a` but reading from it also duplicates the read output
|
||||
into `b`, c.f. `a | tee b` on Unix.
|
||||
NB: if `a` is written to but this stream is never read from,
|
||||
the output will *not* be duplicated. Use this if you only care
|
||||
about the data that was actually read. -/
|
||||
about the data that was actually read.
|
||||
-/
|
||||
def chainRight (a : Stream) (b : Stream) (flushEagerly : Bool := false) : Stream :=
|
||||
{ a with
|
||||
flush := a.flush *> b.flush
|
||||
|
|
@ -66,18 +69,30 @@ end IO
|
|||
|
||||
namespace Lean.Server
|
||||
|
||||
/-- Meta-Data of a document. -/
|
||||
structure DocumentMeta where
|
||||
/-- URI where the document is located. -/
|
||||
uri : Lsp.DocumentUri
|
||||
/-- Version number of the document. Incremented whenever the document is edited. -/
|
||||
version : Nat
|
||||
/-- Current text of the document. -/
|
||||
text : FileMap
|
||||
/--
|
||||
Controls when dependencies of the document are built on `textDocument/didOpen` notifications.
|
||||
-/
|
||||
dependencyBuildMode : Lsp.DependencyBuildMode
|
||||
deriving Inhabited
|
||||
|
||||
/-- Extracts an `InputContext` from `doc`. -/
|
||||
def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
|
||||
input := doc.text.source
|
||||
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
|
||||
fileMap := doc.text
|
||||
|
||||
/--
|
||||
Replaces the range `r` (using LSP UTF-16 positions) in `text` (using UTF-8 positions)
|
||||
with `newText`.
|
||||
-/
|
||||
def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMap :=
|
||||
let start := text.lspPosToUtf8Pos r.start
|
||||
let «end» := text.lspPosToUtf8Pos r.«end»
|
||||
|
|
@ -87,8 +102,10 @@ def replaceLspRange (text : FileMap) (r : Lsp.Range) (newText : String) : FileMa
|
|||
|
||||
open IO
|
||||
|
||||
/-- Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR
|
||||
if that envvar is set. -/
|
||||
/--
|
||||
Duplicates an I/O stream to a log file `fName` in LEAN_SERVER_LOG_DIR
|
||||
if that envvar is set.
|
||||
-/
|
||||
def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := do
|
||||
match (← IO.getEnv "LEAN_SERVER_LOG_DIR") with
|
||||
| none => pure h
|
||||
|
|
@ -150,5 +167,22 @@ def mkApplyWorkspaceEditRequest (params : ApplyWorkspaceEditParams) :
|
|||
|
||||
end Lean.Server
|
||||
|
||||
/--
|
||||
Converts an UTF-8-based `String.range` in `text` to an equivalent LSP UTF-16-based `Lsp.Range`
|
||||
in `text`.
|
||||
-/
|
||||
def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range :=
|
||||
⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩
|
||||
|
||||
open Lean in
|
||||
/--
|
||||
Attempts to find a module name in the roots denoted by `srcSearchPath` for `uri`.
|
||||
Fails if `uri` is not a `file://` uri or if the given `uri` cannot be found in `srcSearchPath`.
|
||||
-/
|
||||
def System.SearchPath.searchModuleNameOfUri
|
||||
(srcSearchPath : SearchPath)
|
||||
(uri : Lsp.DocumentUri)
|
||||
: IO (Option Name) := do
|
||||
let some path := Uri.fileUriToPath? uri
|
||||
| return none
|
||||
searchModuleNameOfFileName path srcSearchPath
|
||||
|
|
|
|||
|
|
@ -202,9 +202,9 @@ section ServerM
|
|||
def eraseFileWorker (uri : DocumentUri) : ServerM Unit := do
|
||||
let s ← read
|
||||
s.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri)
|
||||
if let some path := fileUriToPath? uri then
|
||||
if let some module ← searchModuleNameOfFileName path s.srcSearchPath then
|
||||
s.references.modify fun refs => refs.removeWorkerRefs module
|
||||
let some module ← s.srcSearchPath.searchModuleNameOfUri uri
|
||||
| return
|
||||
s.references.modify fun refs => refs.removeWorkerRefs module
|
||||
|
||||
def log (msg : String) : ServerM Unit := do
|
||||
let st ← read
|
||||
|
|
@ -213,17 +213,17 @@ section ServerM
|
|||
|
||||
def handleIleanInfoUpdate (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
|
||||
let s ← read
|
||||
if let some path := fileUriToPath? fw.doc.uri then
|
||||
if let some module ← searchModuleNameOfFileName path s.srcSearchPath then
|
||||
s.references.modify fun refs =>
|
||||
refs.updateWorkerRefs module params.version params.references
|
||||
let some module ← s.srcSearchPath.searchModuleNameOfUri fw.doc.uri
|
||||
| return
|
||||
s.references.modify fun refs =>
|
||||
refs.updateWorkerRefs module params.version params.references
|
||||
|
||||
def handleIleanInfoFinal (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
|
||||
let s ← read
|
||||
if let some path := fileUriToPath? fw.doc.uri then
|
||||
if let some module ← searchModuleNameOfFileName path s.srcSearchPath then
|
||||
s.references.modify fun refs =>
|
||||
refs.finalizeWorkerRefs module params.version params.references
|
||||
let some module ← s.srcSearchPath.searchModuleNameOfUri fw.doc.uri
|
||||
| return
|
||||
s.references.modify fun refs =>
|
||||
refs.finalizeWorkerRefs module params.version params.references
|
||||
|
||||
/-- Creates a Task which forwards a worker's messages into the output stream until an event
|
||||
which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/
|
||||
|
|
@ -408,31 +408,35 @@ section RequestHandling
|
|||
open FuzzyMatching
|
||||
|
||||
def findDefinitions (p : TextDocumentPositionParams) : ServerM <| Array Location := do
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri
|
||||
| return #[]
|
||||
let references ← (← read).references.get
|
||||
let mut definitions := #[]
|
||||
if let some path := fileUriToPath? p.textDocument.uri then
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
if let some module ← searchModuleNameOfFileName path srcSearchPath then
|
||||
let references ← (← read).references.get
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
if let some ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then
|
||||
definitions := definitions.push definitionLocation
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
if let some ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then
|
||||
definitions := definitions.push definitionLocation
|
||||
return definitions
|
||||
|
||||
def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri
|
||||
| return #[]
|
||||
let references ← (← read).references.get
|
||||
let mut result := #[]
|
||||
if let some path := fileUriToPath? p.textDocument.uri then
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
if let some module ← searchModuleNameOfFileName path srcSearchPath then
|
||||
let references ← (← read).references.get
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
let identRefs ← references.referringTo module ident srcSearchPath
|
||||
p.context.includeDeclaration
|
||||
result := result.append <| identRefs.map (·.location)
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
let identRefs ← references.referringTo srcSearchPath ident
|
||||
p.context.includeDeclaration
|
||||
result := result.append <| identRefs.map (·.location)
|
||||
return result
|
||||
|
||||
/-- Used in `CallHierarchyItem.data?` to retain the full call hierarchy item name. -/
|
||||
/--
|
||||
Used in `CallHierarchyItem.data?` to retain all the data needed to quickly re-identify the
|
||||
call hierarchy item.
|
||||
-/
|
||||
structure CallHierarchyItemData where
|
||||
name : Name
|
||||
module : Name
|
||||
name : Name
|
||||
deriving FromJson, ToJson
|
||||
|
||||
/--
|
||||
|
|
@ -441,13 +445,16 @@ Extracts the CallHierarchyItemData from `item.data?` and returns `none` if this
|
|||
def CallHierarchyItemData.fromItem? (item : CallHierarchyItem) : Option CallHierarchyItemData := do
|
||||
fromJson? (← item.data?) |>.toOption
|
||||
|
||||
private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
private def callHierarchyItemOf?
|
||||
(refs : References)
|
||||
(ident : RefIdent)
|
||||
(srcSearchPath : SearchPath)
|
||||
: IO (Option CallHierarchyItem) := do
|
||||
let some ⟨definitionLocation, parentDecl?⟩ ← refs.definitionOf? ident srcSearchPath
|
||||
| return none
|
||||
|
||||
match ident with
|
||||
| .const definitionName =>
|
||||
| .const definitionModule definitionName =>
|
||||
-- If we have a constant with a proper name, use it.
|
||||
-- If `callHierarchyItemOf?` is used either on the name of a definition itself or e.g. an
|
||||
-- `inductive` constructor, this is the right thing to do and using the parent decl is
|
||||
|
|
@ -461,12 +468,19 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear
|
|||
uri := definitionLocation.uri
|
||||
range := definitionLocation.range,
|
||||
selectionRange := definitionLocation.range
|
||||
data? := toJson { name := definitionName : CallHierarchyItemData }
|
||||
data? := toJson {
|
||||
module := definitionModule
|
||||
name := definitionName
|
||||
: CallHierarchyItemData
|
||||
}
|
||||
}
|
||||
| _ =>
|
||||
let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
|
||||
| return none
|
||||
|
||||
let some definitionModule ← srcSearchPath.searchModuleNameOfUri definitionLocation.uri
|
||||
| return none
|
||||
|
||||
-- Remove private header from name
|
||||
let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName
|
||||
|
||||
|
|
@ -476,22 +490,26 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear
|
|||
uri := definitionLocation.uri
|
||||
range := parentDeclRange,
|
||||
selectionRange := parentDeclSelectionRange
|
||||
data? := toJson { name := parentDeclName : CallHierarchyItemData }
|
||||
data? := toJson {
|
||||
-- Assumption: The parent declaration of a reference lives in the same module
|
||||
-- as the reference.
|
||||
module := definitionModule
|
||||
name := parentDeclName
|
||||
: CallHierarchyItemData
|
||||
}
|
||||
}
|
||||
|
||||
def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams)
|
||||
: ServerM (Array CallHierarchyItem) := do
|
||||
let some path := fileUriToPath? p.textDocument.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
let idents := references.findAt module p.position (includeStop := true)
|
||||
|
||||
let items ← idents.filterMapM fun ident => callHierarchyItemOf? references ident srcSearchPath
|
||||
let items ← idents.filterMapM fun ident =>
|
||||
callHierarchyItemOf? references ident srcSearchPath
|
||||
return items.qsort (·.name < ·.name)
|
||||
|
||||
def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
|
||||
|
|
@ -499,21 +517,19 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
|
|||
let some itemData := CallHierarchyItemData.fromItem? p.item
|
||||
| return #[]
|
||||
|
||||
let some path := fileUriToPath? p.item.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
let identRefs ← references.referringTo module (.const itemData.name) srcSearchPath false
|
||||
let identRefs ← references.referringTo srcSearchPath (.const itemData.module itemData.name) false
|
||||
|
||||
let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do
|
||||
let incomingCalls ← identRefs.filterMapM fun ⟨location, parentDecl?⟩ => do
|
||||
|
||||
let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
|
||||
| return none
|
||||
|
||||
let some refModule ← srcSearchPath.searchModuleNameOfUri location.uri
|
||||
| return none
|
||||
|
||||
-- Remove private header from name
|
||||
let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName
|
||||
|
||||
|
|
@ -524,7 +540,11 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
|
|||
uri := location.uri
|
||||
range := parentDeclRange
|
||||
selectionRange := parentDeclSelectionRange
|
||||
data? := toJson { name := parentDeclName : CallHierarchyItemData }
|
||||
data? := toJson {
|
||||
module := refModule
|
||||
name := parentDeclName
|
||||
: CallHierarchyItemData
|
||||
}
|
||||
}
|
||||
fromRanges := #[location.range]
|
||||
}
|
||||
|
|
@ -547,11 +567,9 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)
|
|||
let some itemData := CallHierarchyItemData.fromItem? p.item
|
||||
| return #[]
|
||||
|
||||
let some path := fileUriToPath? p.item.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
|
||||
let some module ← srcSearchPath.searchModuleNameOfUri p.item.uri
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
|
|
@ -611,12 +629,11 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf
|
|||
|
||||
def handlePrepareRename (p : PrepareRenameParams) : ServerM (Option Range) := do
|
||||
-- This just checks that the cursor is over a renameable identifier
|
||||
if let some path := System.Uri.fileUriToPath? p.textDocument.uri then
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
if let some module ← searchModuleNameOfFileName path srcSearchPath then
|
||||
let references ← (← read).references.get
|
||||
return references.findRange? module p.position (includeStop := true)
|
||||
return none
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← srcSearchPath.searchModuleNameOfUri p.textDocument.uri
|
||||
| return none
|
||||
let references ← (← read).references.get
|
||||
return references.findRange? module p.position (includeStop := true)
|
||||
|
||||
def handleRename (p : RenameParams) : ServerM Lsp.WorkspaceEdit := do
|
||||
if (String.toName p.newName).isAnonymous then
|
||||
|
|
|
|||
|
|
@ -11,10 +11,10 @@ open Lsp
|
|||
|
||||
def identOf : Info → Option (RefIdent × Bool)
|
||||
| .ofTermInfo ti => match ti.expr with
|
||||
| .const n .. => some (.const n, ti.isBinder)
|
||||
| .fvar id .. => some (.fvar id, ti.isBinder)
|
||||
| .const n .. => some (.const `anonymous n, ti.isBinder)
|
||||
| .fvar id .. => some (.fvar `anonymous id, ti.isBinder)
|
||||
| _ => none
|
||||
| .ofFieldInfo fi => some (.const fi.projName, false)
|
||||
| .ofFieldInfo fi => some (.const `anonymous fi.projName, false)
|
||||
| _ => none
|
||||
|
||||
def isConst (e : Expr) : Bool :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue