[isabelle-dev] Feedback from a Isabelle tutorial

Makarius makarius at sketis.net
Fri Jun 24 23:21:00 CEST 2011

On Fri, 24 Jun 2011, Alexander Krauss 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."
>> This behaviour is indeed getting in the way in practice. It works 
>> according to the "specification" of the editing model, but
> What is actually the specification of the editing model? I am just 
> curious here, and if you can explain it quickly, it may give me an 
> intuition of what's happening when something goes "wrong" (i.e., as 
> specified).

The incremental parsing process tries to recognize "command spans", while 
preserving already recognized commands. This means command fragments 
inside an unbalanced quoted entity (" or {*) get "stuck".  The copy-paste 
workaround forces a complete reparse.  There is also an add-on heuristic 
to reparse the current line completely.

The plan is to give up all the special arrangements and reparse the 
visible area eagerly, while treating the invisible one lazyly.


More information about the isabelle-dev mailing list