Stream: Beginner Questions

Topic: jedit not replacing symbols


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jun 20 2024 at 12:31 UTC