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

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 experimentation.

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

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

It makes these completions ambiguous, without any other effect (I think). So there will be a popup, instead of immediate completion.

Maybe we should do this for all "o" and "O" abbrevs at a later stage.


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