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

On Fri, 22 Jan 2016, Makarius wrote:

On Fri, 22 Jan 2016, Makarius wrote:

>   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 \<otimes>.

 I did not know about this odd effect, yet.  It could have been discussed
 long ago.  We are now too close to the actual release for such
 last-minutes changes -- it would require a few weeks/months of

You can try this in $ISABELLE_HOME_USER/etc/abbrevs:

"*o" = ""
"*O" = ""

It makes these completions ambiguous, without any other effect (I think).

In Isabelle2016-RC2 I have clarifiesd that, so an empty assignment always removes all abbreviations (independently of the order).

This is not needed, though, since all "o" and "O" abbreviations are gone. Just too irregular and confusing for such relatively exotic symbols.

The NEWS file contains a few more words on that:

* Symbols â, â, â, â, â, â, â, â no longer provide abbreviations for completion like "+o", "*o", ".o" etc. -- due to conflicts with other
ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.


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