Re: [isabelle] jEdit: Abbreviations
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.
If you count the shift key to get "<", that's 5 keys pressed.
That's my basic solution for getting a right delimiter when the notation
inside the delimiters ends on a character, like
The \<langle> will precede a space, so you can type "lan", but for the
right side, you get "\<rangle>a,bran"
This archive was generated by a fusion of
Pipermail (Mailman edition) and