search

leanprover-community / lean4web

The Lean 4 web editor
https://live.lean-lang.org/
Apache License 2.0
52 stars 14 forks source link

bug: Japanese characters have an incorrect wrapping position. #21

Closed Seasawher closed 1 month ago

Seasawher commented 2 months ago

related #10

Japanese characters have an incorrect wrapping position.

no_wrap wrap

joneugster commented 2 months ago

Sorry, I don't understand from the screenshots what's not working.

Also, could you add some code for copy-pasting and reproducing quicker, please?

Seasawher commented 2 months ago

Sorry. This is the code.

def ja := "いろはにほへとちりぬるをわかよたれそつねならむうゐのおくやまけふこえてあさきゆめみしゑひもせす"

def en := "The quick brown fox jumps over the jazy dog"

def polish := "Pchnąć w tę łódź jeża lub ośm skrzyń fig."

def russian := "В чащах юга жил бы цитрус? Да, но фальшивый экземпляр!"

def chinese := "天地玄黄宇宙洪荒日月盈昃辰宿裂張寒来暑往秋収冬蔵閏余成歳律呂調陽"

I tested again this time and it seems to depend on the font whether this problem is reproduced or not.

Seasawher commented 2 months ago

In other words, if #7 is resolved, this is automatically resolved. This can be considered a duplication of #7.

Seasawher commented 1 month ago

this issue still exists at https://lean.math.hhu.de/.

Seasawher commented 1 month ago

When narrowing the width, line breaks will be inserted.

before_wrap

after_wrap

joneugster commented 1 month ago

I don't consider it a bug that it first wraps at the space before breaking any words, i.e. line 1 in your screenshot seems fine. (although, maybe one could set wrappingStrategy="advanced", see monaco doc)

However, it seems that it wraps japanese & chinese characters wrongly, so that some aren't visible. Right?

joneugster commented 1 month ago

Hmm. Looks like these japanese/chinese characters are treated as double-witdh by monaco, but are only displayed about 1.5x monospace width by the font...

def a := "いろはにほへとちりぬるをわかよたれそつねならむうゐのおくやまけふ"
def b := "天地玄黄宇宙洪荒日月盈昃辰宿裂張寒来暑往秋収冬蔵閏余成歳律呂調陽"
def c := "1122334455667788990011223344556677889900112233445566778899001122"
joneugster commented 1 month ago

wrappingStrategy: "advanced" seems to fix the wrapping of chinese/japanese characters at least :)

Seasawher commented 1 month ago

日本語文字の折り返しを https://lean.math.hhu.de/ でテストしてみた。問題は解決したようだ！ありがとう