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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
