[isabelle-dev] Feedback from a Isabelle tutorial

[Makarius]

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 
improvement.

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.


 	Makarius