[isabelle-dev] Sidekick completion in Isabelle/jEdit
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:
>> 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
More information about the isabelle-dev