Re: [isabelle] RC1: Immediate completion on \-symbols
On Fri, 22 Jan 2016, C. Diekmann wrote:
Type <\> <a> <l> <p> <h> <a>, wait for tooltip, realize I already have
"\<alpha>ha" standing there, delete the "ah".
This odd effect supported the move to the new scheme, but the key
motivation was different: allow working with Isabelle symbols in document
text, without getting insane wrt. LaTeX macros.
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
I've recently seen another odd effect: .o and .O are not immediately
completed, because the dot counts as "word" letter.
I am tempted to remove all these "o" and "O" abbreviations at a later
stage, after Isabelle2016. They are not frequently used, and a bit too
This archive was generated by a fusion of
Pipermail (Mailman edition) and