search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
489 stars 86 forks source link

PG highlights beginning of conclusion like a hypothesis name #640

Open samuelgruetter opened 2 years ago

samuelgruetter commented 2 years ago 
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 commented 2 years ago

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

samuelgruetter commented 2 years ago

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 commented 2 years ago

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

samuelgruetter commented 2 years ago

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...