Re: [isabelle] Unicode tokens in jedit



Hi Lars,

Am Dienstag, den 24.07.2012, 22:37 +0200 schrieb Lars Noschinski:
> On 24.07.2012 17:57, Manuel Eberl wrote:
> > There is one thing about jedit that really annoys me: when I type in an
> > abbreviation of a Unicode token (well, not all of them are Unicode
> > tokens, but you know what I mean), such as -_ or !!, I always have to
> > wait for the auto completion window and then press return for it to be
> > converted to the corresponding Unicode token.
> 
> You can set completion popup delay to 0ms (and then preferable change 
> completion keys from "\n\t " to "\t"); this makes input much more 
> comfortable.

ah, great suggestion, this has been bothering me as well. But I cannot
find this setting anywhere; where would I find it?

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.