Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Document highlight should include identifiers just before cursor #3023

Closed
Kha opened this issue Dec 5, 2023 · 3 comments · Fixed by #5237
Closed

Document highlight should include identifiers just before cursor #3023

Kha opened this issue Dec 5, 2023 · 3 comments · Fixed by #5237
Labels
bug Something isn't working server Affects the Lean server code

Comments

@Kha
Copy link
Member

Kha commented Dec 5, 2023

When placing the cursor at the end of an identifier, we do not send out document highlights, which causes VS Code to serve its own, dumb highlights instead.

image

[Trace - 9:25:36 AM] Received response 'textDocument/documentHighlight - (579)' in 1ms.
Result: []
@Kha Kha added bug Something isn't working server Affects the Lean server code labels Dec 5, 2023
@Kha Kha changed the title Document highlight should include identifiers just after cursor Document highlight should include identifiers just before cursor Dec 5, 2023
@david-christiansen
Copy link
Contributor

While it does make sense to work around limitations in popular tools, this doesn't actually seem wrong to me. I'm also surprised when the thing that the cursor isn't pointing at lights up, though much less so than when random stuff spelled the same lights up!

Can/should we fix it on the VS Code side?

@david-christiansen
Copy link
Contributor

(for clarity: when I say "the thing it isn't pointing at", its because the cursor is on the space after x in your screenshot, not on x)

@mhuisi
Copy link
Contributor

mhuisi commented Dec 5, 2023

We should match what VS Code does here on the language server side.

github-merge-queue bot pushed a commit that referenced this issue Sep 4, 2024
…5237)

Fixes #3023. Also fixes a similar off-by-one in the file worker
definition request.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working server Affects the Lean server code
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants