Re: [isabelle] jEdit: Abbreviations



On 2/14/2013 8:04 AM, Gottfried Barrow wrote:
On 2/14/2013 5:28 AM, Peter Lammich wrote:
How can I configure jEdit to also propose abbreviation replacement
inside words, or at least before special characters such as ' ?

In my concrete case, I'm using greek letter type variables, but whenever
I type: "'gamma", there comes no popup proposing \<gamma>.
The only workaround I currently know is something like typing "' gamma",
and then using backspace to erase the extra space again.
Peter,

You can type \<ga and that will bring it up.

It gets even better. You can type <ga and it will bring up the completion for gamma.

It's reaching over to the "\" with the little finger, followed by having to type "<" that takes up a lot of time. Not having to type "\" is good and will save me substantial time over a period of about 20 years.

Regards





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