From ad8dfa142d539fd714ec0fe43921bfa6881b548f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 2 Sep 2024 16:43:02 +0200 Subject: [PATCH] fix: include identifier before cursor in document highlight request --- src/Lean/Server/FileWorker/RequestHandling.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 5c6a5dc78f69..83fdd3afa6f2 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -315,7 +315,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams) let trees := snaps.map (·.infoTree) let refs : Lsp.ModuleRefs ← findModuleRefs text trees |>.toLspModuleRefs let mut ranges := #[] - for ident in refs.findAt p.position do + for ident in refs.findAt p.position (includeStop := true) do if let some info := refs.get? ident then if let some ⟨definitionRange, _⟩ := info.definition? then ranges := ranges.push definitionRange @@ -324,7 +324,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams) return none return some <| ranges.map ({ range := ·, kind? := DocumentHighlightKind.text }) - withWaitFindSnap doc (fun s => s.endPos > pos) + withWaitFindSnap doc (fun s => s.endPos >= pos) (notFoundX := pure #[]) fun snap => do let (snaps, _) ← doc.cmdSnaps.getFinishedPrefix if let some his ← highlightRefs? snaps.toArray then