[isabelle-dev] Sidekick completion in Isabelle/jEdit

Lars Noschinski noschinl at in.tum.de
Sat Apr 21 02:00:30 CEST 2012


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



More information about the isabelle-dev mailing list