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

leanprover-community / lean4web

The Lean 4 web editor

https://live.lean-lang.org/

Apache License 2.0

52 stars 14 forks source link

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

Closed Seasawher closed 1 month ago

Seasawher commented 2 months ago

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 https://github.com/leanprover-community/lean4web/issues/7#issuecomment-2075498577

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 commented 2 months ago

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 commented 2 months ago

@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 commented 2 months ago

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

aconite-ac commented 2 months ago

@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 commented 2 months ago

joneugster commented 1 month ago

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

Seasawher commented 1 month ago

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

Thanks!

aconite-ac commented 1 month ago

@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!