[isabelle-dev] Feedback from a Isabelle tutorial

Makarius makarius at sketis.net
Fri Jun 24 14:29:10 CEST 2011

On Fri, 24 Jun 2011, Christian Sternagel wrote:

> It is a known issue (if an issue at all) that in Isabelle/jEdit it is 
> sometimes necessary to cut-and-paste some lines in order to 
> "synchronize." Some students found this unexpected or even weren't able 
> to solve exercises in the beginning since they didn't know that the 
> solution was cutting and pasting. After I told them, everything went 
> fine.

This behaviour is indeed getting in the way in practice.  It works 
according to the "specification" of the editing model, but that needs 

Some weeks ago I've got some new ideas for the near future: take the 
existing ways of jEdit to expose or hide parts of the text as hints of 
what needs to be reparsed and rechecked by the prover.  The "folding" and 
"narrowing" of jEdit could then be used effectively to mark the spots 
where updates happen frequently, while other parts will be left untouched.


More information about the isabelle-dev mailing list