[isabelle] Folding by indentation broken in 2016-RC1 [was: Isabelle2016-RC1 available for testing]



Dear Isabelle developers,

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

Example:

lemma x
proof
  have y proof
    (*stuff*)
  qed
  have z sorry proof
    (*stuff*)
  qed
qed

folding at the first proof in line 2 used to yield

lemma x
proof [6 lines]
qed

with 2016-RC1 it yields

lemma x
proof [3 lines]
  have z sorry proof
    (*stuff*)
  qed
qed

and awkwardly moving the proof from line 2 to line 1 and folding there folds the hole proof as expected.

Best
   Benedikt

Am 15.01.16 um 21:27 schrieb Makarius:
Dear Isabelle users,

the coming Isabelle2016 release is scheduled for February 2016. Two weeks after an informal snapshot, we now have a formal release candidate http://isabelle.in.tum.de/website-Isabelle2016-RC1

The corresponding repository versions of Isabelle and AFP are http://isabelle.in.tum.de/repos/isabelle/rev/3764797dd6fc and https://bitbucket.org/isa-afp/afp-devel/commits/2c322507b8a6

The website, NEWS, ANNOUNCE etc. are already up-to-date, but some documentation still needs further revisions.


When discussing problems, observations, suggestions, etc. the mail subject line should be changed to something informative (but the release candidate number still given in the message body).

As usual it is important to keep general laws of causality in mind: release candidates can be modified, but the final release is final.
Testing needs to happen now, in order to be meaningful.


    Makarius






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