Re: [isabelle] jEdit: Abbreviations
> > You can type \<ga and that will bring it up.
Thanks that works
> It gets even better. You can type <ga and it will bring up the
> completion for gamma.
... But this leaves the "<" in place for me, and I end up with
"'<\<gamma>" in the buffer.
I really would like some escape-character that brings up the completions
even inside words, optimally with automatic replacement as I'm used from
This archive was generated by a fusion of
Pipermail (Mailman edition) and