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
PG.


Peter






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