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
