[isabelle-dev] NEWS: Improved completion mechanism
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
More information about the isabelle-dev