[isabelle-dev] Folding in Isabelle/jEdit

Makarius makarius at sketis.net
Thu May 7 11:36:16 CEST 2015


On Wed, 14 Jan 2015, Lars Noschinski wrote:

> I've played around a bit with the folding in Isabelle/jEdit (as of
> 533f6cfc04c0). As far as I can see, one can fold
>
>   - the lemma statement, without the proof
>   - the lemma statement, including the proof
>
> However, my lemma statements usually consists of multiple lines (due to
> being in structured syntax), so the most useful option for me would be:
>
>   - fold the proof, keeping the lemma statement unfolded
>
> Is such a fold available?

I looked at this again, staring a few times at how jEdit manages folds, 
but I did not find a proper way at the moment.  The internal model is a 
bit simplistic.


 	Makarius


More information about the isabelle-dev mailing list