personally, I prefer the new (default) behavior. In Isabelle 2015,
whenever I wanted an alpha, my process was:
, wait for tooltip, realize I already have
ha" standing there, delete the "ah".
In Isabelle 2016, there is still a problem which has been there since
When I want to type the comment (*old*), I type <(> <*>
immediately completes to "(\
". In Isabelle 2016, I would
expect that a tooltip should ask whether to complete the "*o" to
2016-01-22 17:30 GMT+01:00 Peter Lammich
> Hi list,
> in the NEWS I find the following entry.
> * Completion of symbols via prefix of \
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
> 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: <\>
yields greek letter mu immediately
> Isabelle 2016: Only way to get a mu that I know of:
> typing: <\>
[wait for tooltip, .5s by default]
> Am I overlooking something, or is this really the default way for
> entering, e.g., greek letters?