The current [Verbose Lean Grammar](https://github.com/impermeable/waterproof-editor/tree/mapping/src/codeview/lang-pack-verbose) is based on tokens. We should base more on the full structure to improve the highlighting. See the [Rocq-based version](https://github.com/impermeable/waterproof-editor/tree/mapping/src/codeview/lang-pack).
The current Verbose Lean Grammar is based on tokens. We should base more on the full structure to improve the highlighting. See the Rocq-based version.