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 entry:

*** 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 MHonArc.