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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
