Re: [isabelle] RC1: Immediate completion on \-symbols
On Fri, 22 Jan 2016, Lawrence Paulson wrote:
I'm used to using jedit's built-in abbreviation facility.
I am not using that myself, but it is yet another possibility for Peter to
try out. It is described in the jEdit manual.
Could you briefly explain what is different about this new one?
The default completion mechanism of Isabelle/jEdit is not really new,
merely a few policies have been fine-tuned. Thus it has become more
versatile and convenient, with less surprises.
It might require some days/weeks to get used to it, as usual.
This archive was generated by a fusion of
Pipermail (Mailman edition) and