Gergely Buday (Nov 29 2023 at 16:24): Gergely Buday (Nov 29 2023 at 16:24):This worked previously. Today I started Isabelle and when I type => then
\<Rightarrow>
appears but not the Unicode symbol. What should I tweak in some menu?
Gergely Buday (Nov 29 2023 at 16:27):Interestingly, this happens only in my new theory, when I open an old one, the Unicode symbol appears.
Mathias Fleury (Nov 29 2023 at 16:49):File > reload with encoding > utf-8-Isabelle
Mathias Fleury (Nov 29 2023 at 16:50):happens from time to time when the file encoding is not properly identified. Usually when you opened the file with something else than Isabelle/jEdit
Manuel Eberl (Nov 29 2023 at 16:54):When Isabelle/jEdit saves files, it replaces all the unicode symbols with these ASCII replacements. When it loads a file, it substitutes the ASCII replacements with the Unicode symbols again for display. If there are already unicode symbols present in the text file when you load it, this error happens, because it's not supposed to be that way.
Manuel Eberl (Nov 29 2023 at 16:54):As Mathias said, that usually happens when you open an Isabelle file with a text editor and paste some unicode into it and save it.
Gergely Buday (Nov 29 2023 at 17:32):Might it have happened because I imported
imports HOL.Option
but not Main ?
This was a brand new file and I did not touch it with other than Isabelle/jEdit.
Mathias Fleury (Nov 29 2023 at 17:44):Imports have nothing to do with the encoding of the file.
Last updated: May 02 2024 at 04:18 UTC