lean4-mode icon indicating copy to clipboard operation
lean4-mode copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Incorrect highlighting of `dbgTraceIfShared`

Open david-christiansen opened this issue 1 year ago • 1 comments

In this screenshot, the highlighting of dbgTraceIfShared is a bit funky: image

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?

david-christiansen avatar Apr 17 '23 19:04 david-christiansen