irvin (Sep 13 2024 at 23:30): irvin (Sep 13 2024 at 23:30):Seems to work just fine in isabelle/vscode
One example is $ISABELLE_HOME/src/HOL/ex/Chinese.thy . japanese /korean characters also dont work
Further testing by reloading with encoding UTF-8 still doesnt render the characters so maybe might be upstream jedit
Tested on both OSX and linux if that matters.(isabelle2024)
Is it a bug or some issue on my side
irvin (Sep 14 2024 at 00:18):using the file below it seems to be that whole CJK portion is rendered as whitespace
https://github.com/bits/UTF-8-Unicode-Test-Documents/blob/master/UTF-8_sequence_separated/utf8_sequence_0-0xffff_including-unassigned_including-unprintable-replaced.txt
Mathias Fleury (Sep 14 2024 at 04:59):also whitespace for me (under linux)
Mathias Fleury (Sep 14 2024 at 04:59):so bug
Mathias Fleury (Sep 14 2024 at 04:59):but when you report it on the isabelle mailing, call it an "unexpected behavior" not a bug
irvin (Sep 14 2024 at 06:46):Do i submit under dev or user
Mathias Fleury (Sep 14 2024 at 06:48):user
irvin (Sep 14 2024 at 06:51):Thanks i think i managed to send it
Last updated: Dec 21 2024 at 12:33 UTC