Re: [isabelle] Unicode tokens in jedit



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.






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