[Windows] [Chrome] Cursor display position and input position are mismatched

[Seasawher]

I just can't solve it. I'm so confused.

When you try to define longlonglong....name, there was a problem with the cursor "lagging" behind the displayed character.

see #7 (comment)

The bug seems to be caused by a difference between the character width used to calculate the assumed cursor position and the actual character width of the font.

But I don't know how to solve it...

Test Result

• It cannot be reproduced if the OS is Mac.
• Clearing the cache and reloading doesn't help.
• If font is consolas, alphabetic characters are not mismatched, but double-byte characters are mismatched.
• If the font is JuliaMono, full-width characters are not mismatched, but alphabetic characters are mismatched.
• No problem in firefox.

My Environment

• OS: Windows 11 Home
• Browser: latest Chrome

[aconite-ac]

I found the same problem which @Seasawher reported occurs in my similar environment.

Test Result

• Before loading font for displaying source code, this problem doesn't occur.
• When typing a long name such as aaaaaaaaaaaa... , this cursor lagging becomes more serious.
• When viewing a code of markdown file on GitHub, if cursor points a emphasized long sentence, the same problem occurs.
• Both lean4web problem and GitHub problem doesn't occur in firefox.
  (So, it may be a Chrome or Windows problem rather than a lean4web-unique problem.)

My Environment

• OS: Windows 11 Home
• Browser: latest Chrome

[joneugster]

@aconite-ac so you say you observe this in github too, so completely independend of lean4web?

Could it be a bug in the monaco editor?

[joneugster]

Old issues online suggest using monaco.editor.remeasureFonts() once after the font's done loading. I'll try that tomorrow.

[aconite-ac]

@joneugster
I'm not sure their problems about lean4web and GitHub occurs similarly in other environment,
because of my environment is based on Japanese language.

I should have written about it.

Anyway, I thank you for your considering!
I hope this suggestion may solve the problem.

[Seasawher]

related Zulip discussion https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Cursor.20positioning.20is.20broken.20on.20the.20web.20editor

[joneugster]

@Seasawher @aconite-ac could you test the fix that is live on https://lean.math.hhu.de , please?

[Seasawher]

I have tested it, and this issue seems to be resolved.

Thanks!

[aconite-ac]

@joneugster
I have tested it too by long aaaaaaaaaaaa... , some double-byte character , some emoji.
And I found that this issue doesn't occur now.

Thanks!