Unicode replacement in live.lean-lang.org

Stream: general

[Daniel Weber]

When typing \a (note the space after a) in live.lean-lang.org the cursor is placed before the space, instead of after it. This is different from the behavior in vscode, and I find it quite disorienting. Is this change intentional? Is there a way to disable it?
EDIT: this also happens with other characters, e.g. \aq -> αq with the cursor between α and q

[Edward van de Meent]

Indeed. I tend to use space to force the completion, and then remove the added space when necessary. In the playground, this has resulted in multiple occasions in me accidentally removing the character i tried to type, even repeatedly because i didn't get what was going on!

[Damiano Testa]

There was a similar issue about VSCode completion and my recollection was that it was fixed in a not completely robust way.

[Joachim Breitner]

Ping @Jon Eugster

[Alexander Bentkamp]

It's actually much worse: typing 123\a yields 1α .

[Daniel Weber]

Alexander Bentkamp said:

It's actually much worse: typing 123\a yields 1α .

I can't reproduce this, what's your browser?

[Alexander Bentkamp]

Oh, my bad :-). I had espanso running at the same time...

[Alexander Bentkamp]

I fixed the issue here: https://github.com/hhu-adam/vscode-lean4/commit/86303f3a8d3eddc1be1ac3dd98b6c54608c993ad
(and here: https://github.com/hhu-adam/lean4monaco/commit/f1a3ac72d0e673d8f58fd0e1f15409c50e769873)

Still needs some work to get this into lean4web though, and eventually get into live.lean-lang.org.

[Alexander Bentkamp]

Now live at https://lean.math.hhu.de

[Alexander Bentkamp]

@Joachim Breitner (I think you are responsible?) The fix is on the main branch of lean4web now if you would like to update live.lean-lang.org. Make sure to npm install since a dependency has been updated.

[Joachim Breitner]

Deployed, seems to be working.