[isabelle-dev] Missing letters in jEdit

[Jasmin Christian Blanchette]

Dear all,

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

If I change the font or font size, everything is OK. Hence an easy workaround is to do Ctrl++ when that happens, then wait until next time it happens and do a Ctrl+- then. Repeat over time. Hence I can live with that misbehavior.

The letters that vanish are not always the same. Often I only lose one or two capital letters. On the screenshot, much more is missing.

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).

Jasmin