[isabelle] jEdit: Abbreviations



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.


Best,
  Peter






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