Sophie Tourret (Nov 04 2022 at 10:43): Sophie Tourret (Nov 04 2022 at 10:43):I opened jedit on a file this morning and suddently all symbols appear with \<...> instead of the usual nice appearance. Only this one file is affected. Has someone any idea of what can cause that?
Manuel Eberl (Nov 04 2022 at 10:48):Typically this happens when you mix the ASCII-fied symbols (\<…> etc.) that get display by jEdit as unicode symbols but in the file really are just ASCII with actual Unicode symbols. Then the encoding detection fails.
Manuel Eberl (Nov 04 2022 at 10:49):This can happen if you edit a .thy file with another editor and put in Unicode stuff.
Manuel Eberl (Nov 04 2022 at 10:49):Just do File → Reload with Encoding → UTF-8-Isabelle in Isabelle/jEdit. That should fix it.
Last updated: Apr 25 2024 at 20:15 UTC