Re: [isabelle] RC1: Immediate completion on \-symbols
personally, I prefer the new (default) behavior. In Isabelle 2015,
whenever I wanted an alpha, my process was:
Type <\> <a> <l> <p> <h> <a>, wait for tooltip, realize I already have
"\<alpha>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 <(> <*> <o> and it
immediately completes to "(\<otimes>". 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 <lammich at in.tum.de>:
> 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