On 04/21/2012 09:00 AM, Lars Noschinski wrote:
On 20.04.2012 14:29, Makarius wrote:
On Wed, 18 Apr 2012, Christian Sternagel wrote:
The relevant properties are:
sidekick.auto-complete-popup-get-focus=true
sidekick.complete-instant.toggle=false
sidekick.complete-popup.accept-characters=\\n\\t
sidekick.complete-popup.insert-characters=
This already makes quite some improvement over the naive earlier
defaults, i.e. it requires 0 or 1 extra keystrokes to get the intended
result in most situations.
What is interesting is that the GUI focus for the popup does not prevent
from typing regular characters in the text, so even with the convenient
default of true here, it is quite non-intrusive. What I still did not
get is the purpose of \t, since the popup seems to absorb that key
without any effect.
You should be able to use all characters in accept-characters to finish
the completion. I've just \t in there (not \n) and it works fine for me.
I removed \n, as this completes ":" to \<in> at the end of a line (like
in "lemma Foo:\n" ...
I also set "sidekick.complete-delay=0", so I can just keep typing, as I
did in emacs.
For me "\t" does not work as an accept character (nothing happens when I
type "\t"... that's the only reason why I use "\n"). Also, when setting
the delay to 0, I sometimes (nondeterministically it seems) end up in
the situation that jEdit does not react to keystrokes anymore (Mouse is
still working). However this was with jEdit from a few days ago. I did
not yet try with "the new one". (Unfortunately I did not yet find out
how to trigger this bug voluntarily.)
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
