lean4-mode
lean4-mode copied to clipboard
Incorrect highlighting of `dbgTraceIfShared`
In this screenshot, the highlighting of dbgTraceIfShared
is a bit funky:
It seems to me that the issue comes from here, where there is no word-end
in the rx
call, and that dbgTraceIfShared
should be part of lean4-debugging
as well.
Would a PR be welcome with this change?
Also, why do they call eval
? It seems to me that eval
on top of quote
should just be ordinary code. Could that be removed in the same PR?