[isabelle-dev] Feedback from a Isabelle tutorial

[Makarius]

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.


 	Makarius