From bfc185e98e6c88f282586d7f993644ebd7c2fbbf Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 31 Jan 2022 19:48:43 +0100 Subject: [PATCH] fix: don't duplicate definition and declaration requests --- src/Lean/Server/Watchdog.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index bed32092d9..148ced0554 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -536,10 +536,16 @@ section MessageHandling code := ErrorCode.internalError message := s!"Failed to process request {id}: {e}" } + -- If a definition is in a different, modified file, the ilean data should + -- have the correct location while the olean still has outdated info from + -- the last compilation. This is easier than catching the client's reply and + -- fixing the definition's location afterwards, but it doesn't work for + -- go-to-type-definition. if method == "textDocument/definition" || method == "textDocument/declaration" then let params ← parseParams TextDocumentPositionParams params if let some definition ← findDefinition params then (← read).hOut.writeLspResponse ⟨id, #[definition]⟩ + return match method with | "textDocument/references" => handle ReferenceParams (Array Location) handleReference | "workspace/symbol" => handle WorkspaceSymbolParams (Array SymbolInformation) handleWorkspaceSymbol