Skip to content

Commit

Permalink
fix: include identifier before cursor in document highlight request (#…
Browse files Browse the repository at this point in the history
…5237)

Fixes #3023. Also fixes a similar off-by-one in the file worker
definition request.
  • Loading branch information
mhuisi authored Sep 4, 2024
1 parent fa8439a commit d55f55d
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/Lean/Server/FileWorker/RequestHandling.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit d55f55d

Please sign in to comment.