Syntax highlighting

[Alizter]

Various vernac commands are highlighted incorrectly. It's difficult to be exhaustive, so we should keep this issue open to track them. Here are the ones I've come across so far:

• [x] Declare ML Module
• [ ] Set Default Proof Mode
• [ ] Set Strict Universe Declaration
• [ ] Global Set Default Goal Selector "!" highlights Goal and Selector incorrectly separately
• [x] Create HintDb
• [ ] Register
• [ ] Add Search Blacklist
• [x] Add Printing Let
• [x] Hint Unfold
• [x] Scheme
• [x] Opaque
• [x] Monomorphic modifier
• [x] Polymophic modifier

[ejgallego]

This is something we inherit from C.J.'s VsCoq 1, I think that VSCoq 2 also uses the same file; maybe we could sync the effort on Zulip to improve this.

Of course we can add the LSP highlight method (semanticsToken) to coq-lsp, I am not sure about what the mapping for Coq would be.

[4ever2]

This is something we inherit from C.J.'s VsCoq 1, I think that VSCoq 2 also uses the same file; maybe we could sync the effort on Zulip to improve this.

VSCoq 2 also inherited the same file from VSCoq 1, however, all three versions have diverged since then. Interestingly VSCoq 1 seems to have the most up-to-date syntax grammar.

I have a local version of the grammar that fixes several of the issues mentioned and should be mostly up-to-date with Coq 8.20. I'd be happy to open a PR with the changes if you want.

[ejgallego]

Hi @4ever2 , indeed it hasn't been easy to coordinate that; I'd be amazing if you would open a PR updating our definitions!

Please don't forget to update the changelog so your contribution is credited properly.

[ejgallego]

@Alizter we can also implement semantic tokens, that should be easy for commands that are not defined in plugins.

[ejgallego]

Semantic token spec https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_semanticTokens

[ejgallego]

In order to implement semantic tokens in coq-lsp we need to:

• add the different kind of tokens and types to lang, maybe to lang/ast.mli ?
• write a function in coq, maybe in coq/ast.mli that maps Rocq vernaculars to the semantic tokens information.
• implement the semantic token request, add controller/rq_stoken.ml, plug it in lsp_core.ml and add the capability in controller/rq_init.ml.

This will work for the Ast defined in the core Rocq, for plugins, we need to update serlib, I'd be happy to take care of that once we have the basics.