Re: [isabelle-dev] font issues in Isabelle jedit

[Makarius]

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

[Lawrence Paulson]

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

[Lawrence Paulson]

> 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

[Makarius]

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