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

Hover fix #11

Merged
merged 3 commits into from
Oct 22, 2020
Merged

Hover fix #11

merged 3 commits into from
Oct 22, 2020

Conversation

meraymond2
Copy link
Owner

@meraymond2 meraymond2 commented Oct 22, 2020

Problem

On hover, VS tries to type-check the word under the cursor. Unfortunately, it was unaware of where in the code it was, so it would look up words in the middle of strings, comments, etc. Also see #1.

Fix

I think that the ideal fix would be to go through the whole document once and map the ranges of all the non-code blocks. That's not too hard, the tricky bit is maintaining that map after every single document update. (Incidentally, that's a similar problem to handling the semantic highlighting.) But I'm still not sure the best way to map TextDocumentContentChangeEvents to those ranges. Hmm.

So, the short term fix is just to walk the document up to the requested position on every hover. My thoroughly unscientific benchmark showed that it was taking up to 65 ms on the longest file I could find in the Idris2 repo, Vect.idr, which is 900 lines. I wasn't able to perceive the difference, as the Hover has a built in delay anyway.

@meraymond2
Copy link
Owner Author

One thing that slightly confused the testing was that there are plenty of things Idris doesn't return types for, so it's not always obvious that the hover has worked. For example, Nat returns Nat : Type, but String returns 'No such variable String'. It works in the repl, so there might be a work around.

@meraymond2 meraymond2 merged commit 8a07501 into master Oct 22, 2020
@meraymond2 meraymond2 deleted the hover-fix branch October 22, 2020 20:45
@meraymond2 meraymond2 restored the hover-fix branch November 7, 2020 19:47
@meraymond2 meraymond2 deleted the hover-fix branch March 28, 2021 14:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant