feat: textDocument/highlight

[shilangyu]

This LSP request sends a cursor position and expects a list of ranges to be returned that should be highlighted. Usually, LSPs return highlights that correspond to the items semantically equal to the item at the cursor. VsCode sends the textDocument/highlight request every time the cursor moves. If an LSP does not implement this request, by default VsCode will highlight all words in the file that are the same as the word under the cursor. This PR improves on this default behavior by:

1. Disabling this feature in irrelevant contexts (such as comments and string literals)
2. Disabling this for keywords
3. Taking into account Rocq's lexical analysis

I similarly disabled hover and jump to definition in irrelevant contexts (you were able to jump to definition/hover on things in prose of comments and string literals!).

Nr. 3 means that we now properly see e and e' as two different tokens. The default vscode behavior led to the very annoying highlight of unrelated identifiers:

Now, things are properly distinguished:

As future work, it would be better to extend highlight to actual semantic reasoning, not only syntactic.

[shilangyu]

I don't understand what the CI error is

[gares]

Failure seems unrelated

[gares]

Thanks, it looks interesting.
I think there is still a flaw in the sense that let e := ... in let e := ... in e would not properly handle shadowing, but for that one needs a data that is not available yet, the so called glob_term.

I wonder if we could, one day, provide more info, like the type of the selected expression.

[shilangyu]

Thank you for having a look!

I think there is still a flaw in the sense that let e := ... in let e := ... in e would not properly handle shadowing

Yeah, we could try to syntactically differentiate those two es, but that would replicate a lot of logic which would be better to get from some semantic information about these es anyway. I see the current implementation as an incremental improvement over VsCode's default behavior (which would fail here too).

the so called glob_term.

What is that and how would it improve the situation?

[gares]

Rocq does a few passes on the ast, and glob_terms do most of the work about binders & co.