[isabelle-dev] Isabelle/jEdit problem report

Makarius makarius at sketis.net
Fri Feb 17 16:40:00 CET 2012


On Sat, 11 Feb 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).
>
>> 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?
>
> After some experiments, I ended up with the settings for parsing as
> shown in the attached image, which seem to perform quite well.
>
> Previously, the time interval after a key stroke was zero seconds before
> parsing, which is not what you really want in practice anyway.

I understand this as it works for you now.

The plugin options that you have shown are for Sidekick to update its tree 
view.  The "factory defaults" of Sidekick in the official Isabelle bundle 
should be in the green range.

The integration of this classic stateful Java plugin with the stateless 
document model of Isabelle/Scala/jEdit is not as smooth as it could be. 
In the long term I would like to get rid of Sidekick -- it has other 
limitations like a single main buffer, which causes occasional races when 
switching to another editor buffer quickly.


 	Makarius



More information about the isabelle-dev mailing list