Re: [isabelle] RC1: Immediate completion on \-symbols



I'm used to using jedit's built-in abbreviation facility. Could you briefly explain what is different about this new one?

--lcp

> On 22 Jan 2016, at 18:01, Makarius <makarius at sketis.net> wrote:
> 
> you can use the 
> new etc/abbrevs facility to define your own special abbreviations.




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