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.
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
