Re: [isabelle] Folding by indentation broken in 2016-RC1 [was: Isabelle2016-RC1 available for testing]
Am 24.01.16 um 20:57 schrieb Makarius:
I don't really know how "indent" fold mode works: if there is a change
in that respect from Isabelle2015 to Isabelle2016-RC1 it might be an
issue of jedit-5.2.0 vs. jedit-5.3.0.
It worked by folding up to the next line with same or less indentation,
thereby giving the user full control over what needs to be folded away.
In particular it allowed one to fold away cases such that even in a
deeply nested proof with many cases one could have all assumptions made
before on screen at the same time. I.e. folding from a proof to the
That approach was already obsolete in Isabelle2015, see this old NEWS
I wouldn't call it obsolete if it had useful features that the new
method didn't have.
Yes I just tried out the RC2 version, folding from proof to qed works
now fine, which is very nice, but I still can't fold away a case i.e.
to the "next" statement. I could start making case distinctions like
"proof cases assume a show ?case proof - ... qed" but its additional
I think there are 3 mistakes here:
1) Isabelle2016-RC1 has indeed a problem with the fold depth for
proof-qed parentheses, which were not counted as blocks in
Isabelle2015 at all. This should work better with the next release
Yes sorry, messed that up but it wouldn't have made a difference for
folding by indentation.
2) Your example has one 'sorry' too much for proper nesting of proof
structure. Or is this part of the bad situation?
3) I guess that in the experiment, the fold mode was actually
I double checked the fold mode was set to indent, I also switched it
back and forth.
and not "indent".
Or there might be a problem of jEdit selecting the fold mode that
you've had in mind.
Yes, it seems like the setting is ignored or somehow overwritten to
isabelle folding. Even if I select "none" I still get Isabelle folding.
By the way, after updating to RC2 (I need do mention that I'm working of
the isabelle-release repository because I have my bsup/esub display
patch running on top) the jEdit window wouldn't start up after building
HOL and I had to kill and restart the process. Afterwards it started
fine but there was no output panel anywhere, but this might be a side
effect of my old configuration where it was a floating instance.
(Running on OS X by the way)
This archive was generated by a fusion of
Pipermail (Mailman edition) and