[isabelle-dev] NEWS: Improved completion mechanism

Makarius makarius at sketis.net
Tue Sep 3 00:34:51 CEST 2013

On Mon, 2 Sep 2013, Makarius wrote:

>> 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.

Training my fingers a bit more, I've found that the backspace behaviour 
makes it hard to delete keywords that can be completed.  So I am 
considering to get rid of it again.  "Missed" completions can be completed 
via C+b after deletion of bad parts -- I actually did not have C+b when 
trying this at first.

The "hangs" are yet a different story to be sorted out.  I do want to know 
which bleeding edge Linux component is responsible for disrupting Java 
keyboard input.


More information about the isabelle-dev mailing list