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:

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.