From 59f4035ab52386888a4d3b15a43482b6e9879bf5 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Wed, 10 Jan 2024 14:00:02 +0100 Subject: [PATCH] fix: correctly filter local defs from outgoing calls --- src/Lean/Server/Watchdog.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index b5478f3ff55c..57c62954c917 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -498,6 +498,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) let some parentDecl := usage.parentDecl? | return false return p.item.name.toName == parentDecl.name + let outgoingUsages := outgoingUsages.map (·.range) if outgoingUsages.isEmpty then return none @@ -506,7 +507,7 @@ def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams) | return none -- filter local defs from outgoing calls - if item.name == p.item.name.toName then + if item.name == p.item.name then return none return some ⟨item, outgoingUsages⟩