Re: [isabelle] Unicode tokens in jedit



On 07/25/2012 05:37 AM, Lars Noschinski wrote:
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.


Maybe I did not get the original question right. I thought it was: how to obtain unicode tokens faster / by default?

If so, maybe reform to: change completion keys from <whatever> to "\n\t ", since with the previously suggested setting unicode tokens are only inserted when tab ("\t") is pressed (which would be even more inconvenient).

Btw: The settings can be changed in "Plugins -> Plugin Options -> SideKick -> General".

cheers

chris





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