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 "next" statement.
That approach was already obsolete in Isabelle2015, see this old NEWS entry:
I wouldn't call it obsolete if it had useful features that the new method didn't have.
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
     candidate.
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 boilerplate code.
  2) Your example has one 'sorry' too much for proper nesting of proof
     structure.  Or is this part of the bad situation?
Yes sorry, messed that up but it wouldn't have made a difference for folding by indentation.
3) I guess that in the experiment, the fold mode was actually "isabelle"
     and not "indent".
I double checked the fold mode was set to indent, I also switched it back and forth.
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)

Best
  Benedikt




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.