Cursor positioning is broken on the web editor

Stream: general

[Eric Wieser]

When I open the web editor on windows, it seems the cursor layer is out of sync with the text layer; the insertion point when I type is not the one implied by the selection (and the selection also does not align with the characters)

[Eric Wieser]

I can usually fix this by zooming in and out a few times, but this only works until I next refresh

[Jon Eugster]

There's an issue here: https://github.com/leanprover-community/lean4web/issues/24
I don't have access to windows, so it's kinda hard to debug for me.

Nevertheless, I'll try to have a look tomorrow or just revert the fonts to how they were before, it happened when I changed it to JuliaMono.

[Joachim Breitner]

Speaking of JuliaMono I noticed that some emojis in the info view, like when tracing type class resolution, are not colorful and less recognizable. It's only a minor point, of course, but it is one point.

[Jon Eugster]

Maybe there are better font suggestions? I'm not usinng JuliaMono myself but I gathered here on Zulip that it's popular and apparently used by docgen & loogle.

The original issue was that there was no specifically provided font, so it would use whatever the user had installed. Which happend to be non-monospace for some (mac) users, or wouldn't support non-latin scripts (chinese, japanese).

[Eric Wieser]

I agree that JuliaMono is good, and the editor works eventually after some zooms / reloads

[Eric Wieser]

My guess is that Monaco is trying to measure the font size before it loads?

[Jon Eugster]

My guess now (re :cross_mark:) is that I downloaded an incomplete version of JuliaMono, because it shows red in the online glyphs and black when looking at the tff file

[Eric Wieser]

I'm still experiencing this, with the following workaround:

• Let the page load
• Change to some zoom level that wasn't the same as the one the page loaded at.

[Jon Eugster]

Eric Wieser said:

I'm still experiencing this, with the following workaround:

• Let the page load
• Change to some zoom level that wasn't the same as the one the page loaded at.

I got side-tracked into noticing how the vscode-extension part of the web editor is massively outdated and rotting, then got told off from investing time and ended up never pushing a fix for this, sorry :man_facepalming:

[Jon Eugster]

@Eric Wieser is it working correctly for you on https://lean.math.hhu.de now?

[Eric Wieser]

Thanks, seems fixed there

[Joachim Breitner]

Just deployed to live.lean-lang.org, thanks Jon for the ping. Let me know if I broke anything.

[Richard Osborn]

Did you mean live.lean-lang.org? For me it is still broken on Windows. https://lean.math.hhu.de is working with the correct cursor behavior.

[Joachim Breitner]

Ah, maybe I forgot a step. Will try again later today.

[Joachim Breitner]

Can you test again, @Richard Osborn ?

[Richard Osborn]

Seems to be fixed! Thanks!

[Asei Inoue]

@Jon Eugster

now Lean web doesn’t support copy-paste of proof state? I miss that feature.