[isabelle] Isabelle2016-RC0: symbols sometimes displayed as ASCII strings



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

On 01/01/2016 02:17 PM, Makarius wrote:
> Dear Isabelle users,
> 
> the coming Isabelle2016 release is scheduled for February 2016,
> after the next big Java 8 update by Oracle in January and some weeks
> before the deadline of ITP 2016.
> 
> To get started with systematic testing there is now the relatively
> early http://isabelle.in.tum.de/website-Isabelle2016-RC0
> (corresponding to Isabelle/e18444532fce and AFP/c62777f3e932).
> 
> The website, NEWS, ANNOUNCE etc. are already mostly up-to-date.
> Some documentation is still lagging behind, notably the
> Isabelle/jEdit manual. There are further fine points still to be
> sorted out.
> 
> 
> When discussing problems, observations, suggustions, etc. the mail 
> subject line should be changed to something meaningful (but the
> release candidate number still given in the message body).
> 
> As usual it is important to keep general laws of causality in mind: 
> release candidates may still change, but the final release is final. 
> Although this is tautological, in the past few releases we've often
> had complaints right after final lift-off, when it was too late.
> 
> So the best time to start testing is now.
> 
> 
> Makarius
> 


Attachment: signature.asc
Description: OpenPGP digital signature



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