[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 14:16:07 CEST 2014
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.
More information about the isabelle-dev