[isabelle-dev] Isabelle/jEdit problem report
makarius at sketis.net
Thu Jan 19 16:05:29 CET 2012
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?
> 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
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 ...
More information about the isabelle-dev