Syntax highlighting is slow

[jthulhu]

Contrary to most major modes, syntax highlighting in lean4-mode is not instantaneous, in the sense that if I start typing def a : Nat :=, it won't syntax highlight until I have paused my typing, and even then there is a small delay. I haven't read the source code, but this behavior looks like as if syntax highlighting was actually performed by the language server, and passed through lsp, which I suspect is because parsing lean actually requires (at least partially) understanding what is parsed, due to the possible instructions to modify the parsing behavior.

Yet, this feels pretty annoying, and I was wondering if it was possible to make it more snappy.