Email Gateway (Aug 18 2022 at 11:10): Email Gateway (Aug 18 2022 at 11:10):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,
in the new ProofGeneral shipped with the 2007 version, sometimes the
subgoals in the goals-buffer are underlined, sometimes only the
conclusion part of the subgoal.
Has this any meaning ?
Greetings,
Peter
Email Gateway (Aug 18 2022 at 11:10):From: Makarius <makarius@sketis.net>
Very strange. Which version of Emacs is this?
Makarius
Email Gateway (Aug 18 2022 at 11:10):From: Peter Lammich <peter.lammich@uni-muenster.de>
Makarius wrote:
Emacs: [version 21.4.20; December 2006]
ProofGeneral: Version 3.7pre071112.
When I have a reproducible example, I'll also post it. Currently I have
none, because I thought it was some feature, not a bug and did not
isolate one.
regards,
Peter
Email Gateway (Aug 18 2022 at 11:10):From: Peter Lammich <peter.lammich@uni-muenster.de>
Ok, I tracked one example down, it seems to be the case-expression
In the first lemma, everything from the line of the case-expression
onwards is underlined
lemma "(case x of 0 \<Rightarrow> True | Suc i \<Rightarrow> True)" oops
If the next lemma is shown in multiple lines in the subgoals-buffer,
only the line of the case-expression and subsequent lines appear underlined.
lemma
"\<lbrakk>not_underlined;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;many_stuff;
underlined; (case x of 0 \<Rightarrow> True | Suc i \<Rightarrow>
True); also_underlined\<rbrakk> \<Longrightarrow> True"
It seems to be some syntactic matter, not depending on whether constants
are defined or not
regards,
Peter
Peter Lammich wrote:
Last updated: May 03 2024 at 08:18 UTC