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.
Peter,

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

\<langle>a,b\<rangle>

The \<langle> will precede a space, so you can type "lan", but for the right side, you get "\<rangle>a,bran"

Regards,
GB





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