[isabelle-dev] Missing letters in jEdit

[Makarius]

On Tue, 17 Sep 2013, Jasmin Blanchette wrote:

>> Which is the font used in the screenshot?  Is this a standard font by 
>> Apple, or from somewhere else?
>
> It's called Consolas. I believe it's included with Mac OS X 10.8 -- I 
> don't remember installing any special fonts. I had the same issue with 
> Monaco, which is definitely a standard Mac font.

OK, just a few more details: The jEdit Global Options / Text Area pane has 
various "tuning parameters" that affect the font style.  What are your 
preferences for the following?

   Anti Aliased smooth text
   Fractional font metrics


 	Makarius