[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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