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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
