diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index e4bf4a2be795..2482ee9c4efb 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -8,6 +8,7 @@ prelude import Init.Data.List.Control import Init.Data.Range import Init.Data.OfScientific +import Init.Data.Hashable import Lean.Data.RBMap namespace Lean @@ -15,7 +16,7 @@ namespace Lean structure JsonNumber where mantissa : Int exponent : Nat - deriving DecidableEq + deriving DecidableEq, Hashable namespace JsonNumber @@ -205,6 +206,19 @@ private partial def beq' : Json → Json → Bool instance : BEq Json where beq := beq' +private partial def hash' : Json → UInt64 + | null => 11 + | bool b => mixHash 13 <| hash b + | num n => mixHash 17 <| hash n + | str s => mixHash 19 <| hash s + | arr elems => + mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a) + | obj kvPairs => + mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) + +instance : Hashable Json where + hash := hash' + -- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects def mkObj (o : List (String × Json)) : Json := obj <| Id.run do diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index ab1c6602ec17..2af5ae060c85 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -274,7 +274,7 @@ structure CallHierarchyItem where uri : DocumentUri range : Range selectionRange : Range - -- data? : Option unknown + data? : Option Json := none deriving FromJson, ToJson, BEq, Hashable, Inhabited structure CallHierarchyIncomingCallsParams where diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 261e82be7fbe..f5f504241eb5 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -395,6 +395,17 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do result := result.append <| identRefs.map (·.location) return result +/-- Used in `CallHierarchyItem.data?` to retain the full call hierarchy item name. -/ +structure CallHierarchyItemData where + name : Name + deriving FromJson, ToJson + +/-- +Extracts the CallHierarchyItemData from `item.data?` and returns `none` if this is not possible. +-/ +def CallHierarchyItemData.fromItem? (item : CallHierarchyItem) : Option CallHierarchyItemData := do + fromJson? (← item.data?) |>.toOption + private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath) : IO (Option CallHierarchyItem) := do let some ⟨definitionLocation, parentDecl?⟩ ← refs.definitionOf? ident srcSearchPath @@ -406,23 +417,31 @@ private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSear -- 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 -- the wrong thing to do. + + -- Remove private header from name + let label := Lean.privateToUserName? definitionName |>.getD definitionName return some { - name := definitionName.toString + name := label.toString kind := SymbolKind.constant uri := definitionLocation.uri range := definitionLocation.range, selectionRange := definitionLocation.range + data? := toJson { name := definitionName : CallHierarchyItemData } } | _ => let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? | return none + -- Remove private header from name + let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName + return some { - name := parentDeclName.toString + name := label.toString kind := SymbolKind.constant uri := definitionLocation.uri range := parentDeclRange, selectionRange := parentDeclSelectionRange + data? := toJson { name := parentDeclName : CallHierarchyItemData } } def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams) @@ -438,10 +457,13 @@ def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams) let idents := references.findAt module p.position (includeStop := true) let items ← idents.filterMapM fun ident => callHierarchyItemOf? references ident srcSearchPath - return items + return items.qsort (·.name < ·.name) def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) : ServerM (Array CallHierarchyIncomingCall) := do + let some itemData := CallHierarchyItemData.fromItem? p.item + | return #[] + let some path := fileUriToPath? p.item.uri | return #[] @@ -450,24 +472,29 @@ def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams) | return #[] let references ← (← read).references.get - let identRefs ← references.referringTo module (.const p.item.name.toName) srcSearchPath false + let identRefs ← references.referringTo module (.const itemData.name) srcSearchPath false let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl? | return none + + -- Remove private header from name + let label := Lean.privateToUserName? parentDeclName |>.getD parentDeclName + return some { «from» := { - name := parentDeclName.toString + name := label.toString kind := SymbolKind.constant uri := location.uri range := parentDeclRange selectionRange := parentDeclSelectionRange + data? := toJson { name := parentDeclName : CallHierarchyItemData } } fromRanges := #[location.range] } - return collapseSameIncomingCalls incomingCalls + return collapseSameIncomingCalls incomingCalls |>.qsort (·.«from».name < ·.«from».name) where @@ -482,6 +509,9 @@ where def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) : ServerM (Array CallHierarchyOutgoingCall) := do + let some itemData := CallHierarchyItemData.fromItem? p.item + | return #[] + let some path := fileUriToPath? p.item.uri | return #[] @@ -498,7 +528,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) let outgoingUsages := info.usages.filter fun usage => Id.run do let some parentDecl := usage.parentDecl? | return false - return p.item.name.toName == parentDecl.name + return itemData.name == parentDecl.name let outgoingUsages := outgoingUsages.map (·.range) if outgoingUsages.isEmpty then @@ -513,7 +543,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) return some ⟨item, outgoingUsages⟩ - return collapseSameOutgoingCalls items + return collapseSameOutgoingCalls items |>.qsort (·.to.name < ·.to.name) where