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