[isabelle] Bug report. \<^bold>\<lambda> in Cube.thy



I use Isabelle 2018 in Debian. ~~/src/Cube/Cube.thy contains symbol \<^bold>\<lambda> a. k. a. "❙λ" a. k. a "U+2759 U+03BB". This symbol consists of two Unicode code points. When I try to copy this symbol from Isabelle IDE (jEdit), it is very easy to copy second symbol without first, i. e. \<lambda> alone. This symbol looks very like \<^bold>\<lambda> , but has other meaning.

I copy-pasted this symbol to my own theory file and spent a lot of time trying to debug a formula, until I finally saw that \<^bold>\<lambda> and \<lambda> are different symbols.

Currently jEdit works with the symbol \<^bold>\<lambda> badly. When I select this symbol using mouse, only \<lambda> is selected. When I traverse a line containing this symbol using keyboard arrow "Right", I need two key presses to pass this symbol. So, overall support for this symbol in jEdit is bad.

Also, I noticed that other programs deal with this symbol even worse. I write this letter using Chromium on Debian. This Chromium doesn't recognize this symbol at all! I threats it as two symbols. I repeat the symbol as is here: "❙λ". My Chromium renders it as two symbols. So, I wonder whether Unicode standard really says that this symbol should be viewed as one symbol.

So, there is two variants.

1. Unicode standard says that this symbol is one symbol, i. e. it should be rendered as a one symbol, and it contains two code points. Then this means that both Isabelle and my Chromium version has bugs. This means that Isabelle should be fixed one of this ways:

1A. It should handle this symbol as one symbol. This is best variant. (Same applies to other such symbols, of course.)
1B. If you disagree with 1A, i. e. don't want to add proper support to Isabelle, well, then remove such symbols from Cube.thy and other places.

2. Unicode standard says that this is two symbols. This means that my Chromium version doesn't have bugs, i. e. it displays everything properly. But then this means that Isabelle should not display this symbol as one symbol, and that you should not use it in Cube.thy

==
Askar Safin
http://vk.com/safinaskar


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