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