[isabelle-dev] NEWS: Improved completion mechanism

[Makarius]

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 
C+b.


 	Makarius