Re: [isabelle-dev] font issues in Isabelle jedit
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 \ T)) = integral UNIV (\a. if a \ S \ 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 ▩‹\› 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
Re: [isabelle-dev] font issues in Isabelle jedit
I seem to have fixed the problem by selecting File > Reload with encoding > UTF-8-Isabelle Larry > On 2 Jan 2018, at 22:05, Lawrence Paulson wrote: > > But after letting the system build again, the result is the same as before. > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] font issues in Isabelle jedit
> On 2 Jan 2018, at 19:21, Makarius wrote: > > I have changed the fonts again recently, see Isabelle/ecb74607063f. I've > made a brief test on my MacMini with High Sierra, and it appears to work. > > > Normally "isabelle components -a" should give you the resulting ttf > files, and Isabelle/jEdit should pick them up. > > This can be prevented by having IsabelleText.ttf / IsabelleTextBold.ttf > installed on the system by accident (on macOS in some Library/Fonts > directory, FontBook should be able to tell you). You should remove such > spurious copies of the Isabelle fonts. I didn’t have any copies in those places, but I deleted all the copies in the contib directory, did “hg fetch” and finally ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: "/Users/lp15/.isabelle/contrib/isabelle_fonts-20171230" Getting "https://isabelle.in.tum.de/components/isabelle_fonts-20171230.tar.gz"; Unpacking "/Users/lp15/.isabelle/contrib/isabelle_fonts-20171230.tar.gz" ~/isabelle/Repos/src/HOL: hg id 17fdb2c98083 tip But after letting the system build again, the result is the same as before. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] font issues in Isabelle jedit
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 \ T)) = integral UNIV (\a. > if a \ S \ T then 1::real else 0)" > > Any idea what could be wrong? I’m using > >> 6afba546f0e5 tip I have changed the fonts again recently, see Isabelle/ecb74607063f. I've made a brief test on my MacMini with High Sierra, and it appears to work. Normally "isabelle components -a" should give you the resulting ttf files, and Isabelle/jEdit should pick them up. This can be prevented by having IsabelleText.ttf / IsabelleTextBold.ttf installed on the system by accident (on macOS in some Library/Fonts directory, FontBook should be able to tell you). You should remove such spurious copies of the Isabelle fonts. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] font issues in Isabelle jedit
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 \ T)) = integral UNIV (\a. if a \ S \ T then 1::real else 0)" Any idea what could be wrong? I’m using > 6afba546f0e5 tip Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev