meraymond2
commented
4 years ago 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.
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 https://github.com/meraymond2/idris-vscode/issues/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.