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
Isabelle 2015:

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>:
> 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?
> Example:
> 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?
> --
>   Peter

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.