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

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


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