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