Re: [isabelle] Unicode tokens in jedit



On 25.07.2012 09:06, Joachim Breitner wrote:
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?

Plugins / Plugin Options / SideKick / General.

Under Code Cmopletion Options, set "After popup trigger keystrowk, wait" to 0.0; enable "Automatic completion popups get focus".

  -- Lars





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