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