[isabelle-dev] NEWS: more informative errors in lazy enumerations

Makarius makarius at sketis.net
Mon Nov 26 11:35:24 CET 2012

On Fri, 23 Nov 2012, Lars Noschinski wrote:

> On 20.11.2012 16:05, Makarius wrote:
>> What might happen before the release is a move from Sidekick/completion
>> subplugin, to the new Completion standalone-plugin from the jEdit guys.
>> It depends if their release schedule recovers after the summer break --
>> I don't see any important activity there since 01-Sep-2012, whicj was
>> the original plan for jEdit 5.0 to be rolled out.
> It seems to have recovered just half an hour ago.

I've updated myself to this jedit-5.0.0 release, and will do so for 
Isabelle/jEdit when I am sufficiently convinced that it is really stable.

BTW, the Completion plugin that lead to this side-thread was a 
misunderstanding of mine: someone forked it off the Sidekick subplugin 
some years ago, but it was not updated recently.  It adds a few features, 
such as immediate completion without pupup, but also some problems.

The "completion service" is forked as independent thread, but that has to 
access the mutable buffer to read its content and potentially some GUI 
components.  So it is the usual problem of Scylla and Charybdis in 
concurrent programming with mutable state: lock too little and hope for 
the best (that the user is typing slowly), or lock too much and lock-up 
the application in the worst case.

Mutability sucks ...


More information about the isabelle-dev mailing list