Fix incorrect syntax highlighting on lean4-debugging keyword

[casavaca]

I also encountered #36 and decided to give it a try.

How the bug was introduced

The original code was added in leanprover/lean4@ba4fdce , where you can see (defconst lean4-debugging '("unreachable" "panic" "assert" "dbgTrace") "lean debugging") corresponds to

@[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace    := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
@[builtinTermParser] def assert      := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser

This is where the we should improve into

-(defconst lean4-debugging '("unreachable" "panic" "assert" "dbgTrace") "lean debugging")
-(defconst lean4-debugging-regexp
-  (eval `(rx word-start (or ,@lean4-debugging))))
+(defconst lean4-debugging '("unreachable!" "panic!" "assert!" "dbgTrace!") "lean debugging")
+(defconst lean4-debugging-regexp
+  (eval `(rx word-start (or ,@lean4-debugging) word-end)))

How to fix it

Now, the other 3 builtin terms didn't change, but dbgTrace! was renamed to dbg_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.

1. Why switch the order?
   This is because lean4-constants-regexp would already fontify !, so that later lean4-debugging won't fontify those with an ! again.
2. Why after the fix, you won't actually see font-lock-warning-face as if it is not working?
   The code is actually working, but overwritten by lsp server. In da21b10, we enabled lsp-semantic-tokens-enable, which is an alias of lsp-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:

[casavaca]

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.

[mekeor]

This looks good to me. Let's merge it.