Open casavaca opened 6 months ago
Note that we may want to keep font-lock-warning-face
for panic
(from Init.Prelude) or dbgTrace
(from Init.Util) or both. These are not overwritten by lsp server and are displayed correctly. In that case, we can just add panic
or dbgTrace
into line 68.
This looks good to me. Let's merge it.
I also encountered #36 and decided to give it a try.
How the bug was introduced
The original code was added in https://github.com/leanprover/lean4/commit/ba4fdce508351bb222e58769fa1ce19a938a1f96 , where you can see
(defconst lean4-debugging '("unreachable" "panic" "assert" "dbgTrace") "lean debugging")
corresponds toThis is where the we should improve into
How to fix it
Now, the other 3 builtin terms didn't change, but
dbgTrace!
was renamed todbg_trace
(https://github.com/leanprover/lean4/blob/6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a/src/Lean/Parser/Term.lean#L781)That explains line 68-70. But there are 2 more things to explain.
lean4-constants-regexp
would already fontify!
, so that later lean4-debugging won't fontify those with an!
again.lsp-semantic-tokens-enable
, which is an alias oflsp-enable-semantic-highlighting
. It should work correctly when lsp server is not present. (I tested using https://github.com/Lindydancer/font-lock-studio)look and feel:
before the fix:
after the fix: