[isabelle] RC1: Immediate completion on \-symbols

Hi list,

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?

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> 

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