Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] proof state layout


view this post on Zulip Email Gateway (Jul 24 2020 at 11:34):

From: Tobias Nipkow <nipkow@in.tum.de>
When I look at how proof states are displayed in the document prog-prove.pdf
dated April 29 it looks like it always did. However, when I produced the same
document today I find that the pretty printer no longer inserts line breaks in
subgoals but displays them as one long line. For example on page 11. What
happened and how can I get the line breaks back?

Tobias
smime.p7s

view this post on Zulip Email Gateway (Jul 26 2020 at 20:42):

From: Makarius <makarius@sketis.net>
OK, this is a consequence of pide_session=true, which is now enabled by default.

I have updated the latex pretty-printing accordingly, so it should work again, see
https://isabelle-dev.sketis.net/rISABELLE9c0b835d4cc2

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 28 2020 at 05:54):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, back to normal!

Tobias
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC