Email Gateway (Aug 22 2022 at 12:27): Email Gateway (Aug 22 2022 at 12:27):From: Giuliano Losa <giuliano@losa.fr>
Dear Makarius,
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.
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. Using
auto-completion results in uninterpreted symbols begin displayed by
Isabelle/jEdit. 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.
I am using Debian stable.
Giuliano
signature.asc
Email Gateway (Aug 22 2022 at 12:28):From: Makarius <makarius@sketis.net>
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:
paragraph ‹Encoding.›
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
by Isabelle/jEdit.
This works as intended: absence of Isabelle encoding means you see symbols
literally.
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.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC