Unicode input issue

[buggymcbugfix]

PS'': When I try to write identityʳ, when I do \ ^ r after identity, I get this: I then have to do right arrow on my keyboard to get identityʳ. Is this a bug or some sort of font issue?

[banacorn]

I'm not sure is that a bug or some sort of font issue, maybe both?

It seems to happen only when we are trying to add these diacritics on top of the symbols preceding them.

[rwe]

This is a bug, I encounter this too when I do it for \^r or \^l. I end up having to manually copy and paste it.

[rwe]

Ok, I have not tracked this issue down but I can provide some additional information and repro steps. I noticed something interesting: clicking the symbol in the input method correctly inserts the character.

Key Sequence	UI State
\
\^
\^r
\^r (Hover)
\^r (After click)

If I select those squares (which select as a single character), copy the value, and paste into xxd:

pbpaste | xxd -

The result is:

00000000: 79e2 8397                                y...

Which is 79 (y) plus a combining character e2 8397 (COMBINING RIGHT ARROW ABOVE).

The result of the entire editor text is:

00000000: 6964 656e 7469 7479 e283 97ca b3         identity.....

Note that the ca b3 is the UTF-8 encoding of the intended ʳ character. (https://www.compart.com/en/unicode/U+02B3)

Interestingly, when I just copied from Atom and pasted into vim, it looks like so:

Which shows the arrow combining character more clearly.

[rwe]

Additional info: This does not appear to be a font issue (at least, not strictly). The text shows up visibly in Vim and my console and they're the same font as in Atom, and changing Atom's font between several common ones like Menlo, Consolas, etc. does not fix the issue.

I've confirmed that Atom is set to UTF-8. I'm beginning to think this might be a purely Atom/Chrome issue (wrt to correctly displaying the combining right arrow). For example, I see squares on this page in Chrome: https://tex.stackexchange.com/questions/171356/using-unicode-combining-right-arrow-above-to-generate-vector-command

So perhaps the "bug" here is just that agda-mode attempts to use that character, which it should reasonably be allowed to do. And the secondary cause is that it prefers that character to the intended superscript r.

[banacorn]

Wow, didn't realize that the problem is that deep.

I'm currently working on refactoring and writing tests for the unicode input, and I'm planning to fix (or workaround, in this case) all related issues along the way.

[banacorn]

All 4 ^r symbols can be displayed without much problem in Atom/Chrome when placed standalone. But some are problematic (boxes) when combined with some other characters:

standalone	unicode hex	combined	unicode hex
⃗	20d7	a⃗	61 20d7
⃑	20d1	a⃑	61 20d1
⃕	20d5	a⃕	61 20d5
ʳ	2b3	aʳ	61 2b3

Because all these 4 symbols share the same sequence ^r, they appear as "candidates" as seen in the bottom right. And the first candidate would be displayed as some kind of preview on the text editor. This explains the boxes you are seeing when you type ^r.

You should see the displayed preview changing (not in this case as they all appear box-ish except for the last) as you navigate through the candidates (by pressing the arrow keys on your keyboard).

I suppose that ʳ is the most wanted symbol among these 4 symbols. I think placing ʳ as the first candidate would solve most of our problems.

[banacorn]

A more general way of solving this.