[isabelle-dev] Isabelle/jEdit problem report

[Makarius]

On Sun, 8 Jan 2012, Florian Haftmann wrote:

> jEdit freezes after fast keystrokes in sequence in big theories: no
> reaction on keyboard or mouse events, mouse pointer disappears; cpu load
> of both poly and jvm processes is not conspicious.
>
> Reproduction: Open List.thy with HOL-Plain as base image, edit something
> in the middle of the theory; seems to occur in connection with dangling
> quotes (i.e. after a opening quote the closing one is not yet there,
> turning the remainder of the theory into a mess).
>
> Maybe race condition?
>
> Revisions:
> 	jdk1.6.0_21
> 	scala-2.8.2.final
> 	jedit_build-20111217
> 	Isabelle rev. f58b7f9d3920

I have tried once more with this version, but failed to reproduce it.  If 
it is a timing problem than it would be hard anyway.  How many cores do 
you have?  Does the problem persist, say in Isabelle/8fbcbcf4380e from 
today?


The quote-mismatch thing can also cause some visual confusion, because the 
static tokenizer of jEdit displays defines boundaries differently than the 
semantic markup by the prover.

What is also special about List.thy is its sheer size.  So any of the 
concurrent editing tasks might take longer than otherwise, and make it 
easier to get into a problem than usual.


Anyway, I am on travel in the next 3 weeks ...


 	Makarius