Re: [isabelle] Folding by indentation broken in 2016-RC1 [was: Isabelle2016-RC1 available for testing]
On Wed, 20 Jan 2016, bnord wrote:
as the Isabelle/jEdit folding feature has no support for folding proofs based
on proof structure I used to use indentation based folding in jEdit.
That approach was already obsolete in Isabelle2015, see this old NEWS
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved folding mode "isabelle" based on Isar syntax. Alternatively,
the "sidekick" mode may be used for document structure.
In 2016-RC1 this seems to be broken and I get very wired folding that
doesn't correspond to my indentation. I enabled "fold mode: indent" in
the global editing options.
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
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 "isabelle"
and not "indent".
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.
Or there might be a problem of jEdit selecting the fold mode that you've
had in mind.
This archive was generated by a fusion of
Pipermail (Mailman edition) and