From 6caf6d6c62638117d3574be4eb36b96dffbc6bfc Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 2 Sep 2024 16:47:11 +0200 Subject: [PATCH] fix: include identifier before cursor in definition request The watchdog definition request already does this correctly, but when the request falls through to the file worker, it wouldn't use the identifier before the cursor. --- src/Lean/Server/FileWorker/RequestHandling.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 83fdd3afa6f2..8db908b87931 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -223,7 +223,7 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - withWaitFindSnap doc (fun s => s.endPos > hoverPos) + withWaitFindSnap doc (fun s => s.endPos >= hoverPos) (notFoundX := pure #[]) fun snap => do if let some infoWithCtx := snap.infoTree.hoverableInfoAt? (omitIdentApps := true) (includeStop := true /- #767 -/) hoverPos then locationLinksOfInfo kind infoWithCtx snap.infoTree