On Fri, 27 Jun 2014, Peter Lammich wrote:
* "Disappearing Proofs" in PG is a really nice feature to keep overview,
in particular in larger files. In PG, I used it heavily. There is
nothing similar in Isabelle/jEdit. Code-folding can be used to a
certain extent, but it cannot handle apply-style proofs, and is not
applied automatically as in PG.
Moreover, code-folding still seems not to work properly: Sometimes,
fold-markers simply do not appear, sometimes they appear at completely
wrong places. I'm not sure whether this is a non-deterministic effect,
or depends on some garbage text at the end of the theory file.
jEdit has some fold support, but the Isabelle/jEdit version of it is still
in the adhoc state of 2010, i.e. very basic and hardly usable.
I tried again for the coming release to make more of this work, but I got
entangled into too many other problems. This is also the reason, why I
have started to spend signigicant time to make a clear slate, and
eliminate the remaining uses of Proof General first.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
