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
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and