[isabelle-dev] NEWS: Improved completion mechanism
makarius at sketis.net
Mon Sep 2 11:30:18 CEST 2013
On Sat, 31 Aug 2013, Christian Sternagel wrote:
> First note that for me keyboard input to Isabelle/jEdit typically hangs
> every 10 minutes or so, depending on how fast I type (but this is an old
> and known issue).
I was hoping that it would have disappeared altogether. So far the
speculation was that the "hang" is due to the window manager and its
built-in conflicts with JWindow etc. The popups are now done without
separate window, as plain Swing JComponent. So the persisting "hang"
indicates some problem in more elementary key hangling or plain text
insertion into the text buffer.
I have myself done a lot of empirical tests recently on several quite
different systems, and I am also typing very fast, but did not see any
problem like that.
It looks like we need to make another round in the game of guessing at
oddities that Fedora Linux might have installed.
> In Isabelle2013 the completion popup was not triggered when deleting
> characters (with backspace). Now this is the case and it seems to cause
> more frequent hangs for me (since deleting is typically done very fast).
> Is this behavior intentional, and if yes, what is the gain?
SideKick had a special flag for backspace treatment, which was off by
default. By not using SideKick anymore that behaviour came out naturally
from the way things work. I have observed the change myself, and started
thinking if it is good or bad. So far I consider it as good -- a more
natural flow of typing, e.g. when potential completions are accidentally
"missed" in the first attempt.
Generally, there is quite a difference in the completion behaviour with
the 3 options for it, and the possibility to do explicit completion via
More information about the isabelle-dev