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:

• Declare ML Module
• Set Default Proof Mode
• Set Strict Universe Declaration
• Global Set Default Goal Selector "!" highlights Goal and Selector incorrectly separately
• Create HintDb
• Register
• Add Search Blacklist
• Add Printing Let
• Hint Unfold
• Scheme
• Opaque
• Monomorphic modifier
• 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.