Suggestion: rocq-lsp in mv files could distinguish blocks of code and rest of document in UI #1080
Description
Hi, I know the project is currently pending transfer to new maintainers, but I'm posting this issue in case someone has the time to do something about it in the future. It is non-urgent.
I had a student working on an .mv file get confused because rocq-lsp was reporting No goals at this point in a block of Proof. Qed. As it turned out, the issue was the rocq-lsp did not consider the block to be Rocq code, because the block of code started with ```rocq (there was a space after rocq).
I don't suggest fixing specifically this case, but rather making it clearer in the UI when we are in a Rocq block or not. E.g., outside a Rocq block, rocq-lsp could print Not in a block of Rocq code or nothing at all, instead of printing No goals at this point.