Re: [isabelle] RC1: Immediate completion on \-symbols


Note that there was an immediate completion flag, and the alpha would actually appear after typing \alp without any waiting for tooltips or pressing of tab or ctrl-b.

Of course, as you report, the backside was that some things where completed too eagerly.

However, if you type a backslash in Isabelle, you almost always want a completion. The new behaviour makes it just more typing to get it.

In my opinion, one imperfect method wad replaced by another one, but no method is strictly better than the other. And for me, the old method workedwith less typing overhead, that is why I want it back.


-------- Originalnachricht --------
Betreff: Re: [isabelle] RC1: Immediate completion on \-symbols
Von: "C. Diekmann"
An: Peter Lammich
Cc: isabelle-users


personally, I prefer the new (default) behavior. In Isabelle 2015,
whenever I wanted an alpha, my process was:

Type <\>

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

When I want to type the comment (*old*), I type <(> <*> and it
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?
> Example:
> 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?
> --
> Peter

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