[isabelle] RC1: Immediate completion on \-symbols
in the NEWS I find the following entry.
* Completion of symbols via prefix of \<name> or \<^name> or \name is
always possible, independently of the language context. It is never
implicit: a popup will show up unconditionally.
In practice this means that I have to type lots of additional <tabs>,
and set the completion tooltip delay to 0, in order to efficiently enter
symbols via \-abbreviations. Note that, in particular greek letters, are
solely accessible via their \-abbreviations.
Is there a way to get the old behaviour back, where the symbol is
completed immediately if the abbreviation is unique?
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>
Am I overlooking something, or is this really the default way for
entering, e.g., greek letters?
This archive was generated by a fusion of
Pipermail (Mailman edition) and