[isabelle-dev] Sidekick completion in Isabelle/jEdit

Christian Sternagel c-sterna at jaist.ac.jp
Sat Apr 21 02:53:58 CEST 2012


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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list