PG highlights beginning of conclusion like a hypothesis name

[samuelgruetter]

Notation "a -:" := (id a) (at level 9, format "a -:").
Lemma test(foo: nat) : foo-: = foo.

displays

  foo : nat
  ============================
  foo-: = foo

where the foo- part of the last line is printed in bold orange (the same font as hypothesis names), and at the :, it changes back to normal font. Desired behavior: No highlighting should occur in the conclusion.

PG version: a61a1d8e5ffa610b794535995d58adf18e9ec47b of Fri Dec 17 2021

My guess is that there's a slightly too general regex somewhere?

[Matafou]

Indeed the regexp is a simplistic for efficiency reasons. I will make some experiments.

[samuelgruetter]

Ah I see, and I agree that preferring simple regexes for performance reasons makes sense, because when I work on interactive proofs with large goals, it often happens that a lot of time is spent in the emacs process, which I suspect could be exactly such regex processing.

[Matafou]

Interesting. How big are your goals please? I think you can turn off syntax highlighting in goals if it is to annoying.

[samuelgruetter]

When my proof scripts contain no bugs, the goals are usually quite small and printed instantly. Printing slowness occurs when I have a bug in a proof script and some definitions that shouldn't be unfolded are unfolded, or cbv/vm_compute is called on a term that's not concrete enough, and such goals can get really big. If I remember correctly, I recently had one that got truncated at around 130K lines...