[isabelle] Unicode tokens in jedit



Hallo,

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.

This, frankly, is rather annoying since I don't need auto completion
anyway. I already set the completion dialogue delay to 0 and that helps
a bit, but I still have to press return every time and that's annoying.
I want jedit to replace the abbreviations with the corresponding Unicode
tokens immediately when I type them, like Proof General does, since this
enables me to type much faster.

Is there a way to do this, and if not, is it possible to add an option
for this in future releases of jedit?

Cheers,
Manuel





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