Skip to content

Commit

Permalink
fix: include identifier before cursor in definition request
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
mhuisi committed Sep 2, 2024
1 parent ad8dfa1 commit 6caf6d6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion 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

0 comments on commit 6caf6d6

Please sign in to comment.