Re: [isabelle] Isabelle2016-RC0: symbols sometimes displayed as ASCII strings
On Thu, 7 Jan 2016, Giuliano Losa wrote:
I started using Isabelle2016-RC0 on Debian stable and it worked fine
until today, when Isabelle/jEdit stopped interpreting symbols as Unicode
glyphs in the main window, but only for one particular theory file.
Other theory files are still displayed using Unicode glyphs and so is
the text in the output panel, even when the problematic theory file is
displayed in the main window.
I don't think there is anything new here in Isabelle2016-RC0, although the
underlying jEdit version has changed. The situation is explained in the
Isabelle/jEdit manual as follows:
text âTechnically, the Unicode view on Isabelle symbols is an ââencodingâ
called ââUTF-8-Isabelleâ in jEdit (not in the underlying JVM). It is
provided by the Isabelle/jEdit plugin and enabled by default for all source
files. Sometimes such defaults are reset accidentally, or malformed UTF-8
sequences in the text force jEdit to fall back on a different encoding like
ââISO-8859-15â. In that case, verbatim ``ââÎâ'' will be shown ithtext
buffer instead of its Unicode rendering ``âÎâ''. The jEdit menu operation
ââFile~/ Reload with Encoding~/ UTF-8-Isabelleâ helps to resolve such
problems (after repairing malformed parts of the text).
New symbols entered in the problematic theory file using the symbols
panel are displayed as Unicode glyphs, but, upon saving the file, they
result in Unicode characters in the raw source file.
This is indeed a bit confusing. I will refine the Symbols panel to insert
uninterpreted Isabelle symbols instead, when the Isabelle encoding is off.
Using auto-completion results in uninterpreted symbols begin displayed
This works as intended: absence of Isabelle encoding means you see symbols
Editing the raw source file to get rid of all Unicode characters and
reloading does not fix the problem, but copying the files somewhere else
in the file-system fixed it.
jEdit has a persistent store for that in recent.xml of the so-called
settings directory, e.g. see the menu Utilities / Settings Directory.
Sometimes the global default of UTF-8-Isabelle is ignored. It might be
interesting to see why it happened in this particular file.
This archive was generated by a fusion of
Pipermail (Mailman edition) and