On 02/01/18 19:34, Lawrence Paulson wrote: > Fonts have been weird for me for some time (clearly wider than jedit “thinks” they are) but now symbols are completely missing. E.g. I see > > have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
On 03/01/18 23:22, Lawrence Paulson wrote: > I seem to have fixed the problem by selecting > > File > Reload with encoding > UTF-8-Isabelle I have misunderstood your original problem description: it was not about fonts, but the character encoding. I have also refined that recently, see Isabelle/3cf05d7cf174 with the following text in the Isabelle/jEdit manual: > Technically, the Unicode interpretation of Isabelle symbols is an > ∗‹encoding› called ▩‹UTF-8-Isabelle› in jEdit (∗‹not› in the underlying > JVM). It is provided by the Isabelle Base plugin and enabled by default for > all source files in Isabelle/jEdit. > > 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 in the text > 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). > > If the loaded text already contains Unicode sequences that are in conflict > with the Isabelle symbol encoding, the fallback-encoding UTF-8 is used and > Isabelle symbols remain in literal ▩‹\<symbol>› form. The jEdit menu > operation ∗‹Utilities~/ Buffer Options~/ Character encoding› allows to > enforce the UTF-8-Isabelle, but this will also change original Unicode > text into Isabelle symbols when saving the file! Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev