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

On Fri, 22 Jan 2016, Peter Lammich wrote:

Is there a way to get the old behaviour back, where the symbol is completed immediately if the abbreviation is unique?

No. "To get the old behaviour back" is one of these dangerous phrases that provoke short answers.

There were various reasons for this simplification of completion, and after a little bit of practice it feels very natural. It generally reduces the surprise in different completion contexts, e.g. in document sources with embedded antiquotations.

Isabelle 2015:
 typing: <\> <m> <u> yields greek letter mu immediately

Isabelle 2016: Only way to get a mu that I know of:
 typing: <\> <m> <u> [wait for tooltip, .5s by default] <tab>

"The only way" is another dangerous phrase. For example you can use the new etc/abbrevs facility to define your own special abbreviations. Non-word abbrevs are immediate as before, but depend on the completion context.

Explicit completion is unchanged: you can use C-b after a sufficiently long prefix to complete it.


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