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