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