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