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 https://github.com/leanprover/lean4/commit/ba4fdce508351bb222e58769fa1ce19a938a1f96 , 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 da21b1037, 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: