[isabelle-dev] Missing letters in jEdit

[Makarius]

On Tue, 17 Sep 2013, Jasmin Christian Blanchette wrote:

> I have moved to jEdit about one month ago. One bug that pops up now and 
> then is that some letters are not displayed (on Mac OS 10.8). This has 
> happened irregularly over the entire month. The screenshot below as 
> taken against d4a4b32038eb:
>
>    http://www21.in.tum.de/~blanchet/missing_letters.png

This looks really bad, and needs to be investigated further.  I've not 
seen such a bad visual drop-out in the past 1-2 years, despite many minor 
mistakes in the painting of Java on many different platforms.

I might be also responsible myself, potentially doing some text painting 
too ambitously or improperly according to Java 2D standards.  (All text 
that you see in Isabelle/jEdit is painted by the Isabelle plugin, not the 
standard painter of jEdit.)


> The same seems to happen irrespectively of the font I'm using, although 
> I'm not sure if I ever ran into the issue with IsabelleText (whose 
> letters are not quite as crisp at low sizes as many other fonts 
> installed on my machine).

We should start looking there, and pin down fonts that tend to cause 
problems vs. fonts that work.

Which is the font used in the screenshot?  Is this a standard font by 
Apple, or from somewhere else?


 	Makarius