[isabelle-dev] NEWS: more informative errors in lazy enumerations
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