Re: [isabelle] Unicode tokens in jedit
On 25.07.2012 09:42, Christian Sternagel wrote:
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
This is all a matter of preference, but I prefer to use \t only as a
completion character, as otherwise I need to take care to avoid
completion in certain situations (the colon in lemma names, ML code ,...).
This archive was generated by a fusion of
Pipermail (Mailman edition) and