Re: [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
On Tue, 26 Jan 2016, Clemens Ballarin wrote:
The font metrics in the Search and Replace dialog has been funny for a
while, and this is still the case with RC2's versions of jdk, jedit and
fonts. In the attached screenshot, the entire text is selected but the
last 2 1/2 characters are not covered by the box.
MacBook Pro (Retina, 13-inch, Early 2015) and OS X 10.10.5.
Is that Isabelle/jEdit in the default configuration?
There should be the IsabelleText font in the main text area, as well as in
the small text field of the search dialog. jEdit plays some special
tricks to achieve that.
In the screenshot the font in the text field is a different one: it looks
more like the default one by Apple.
This archive was generated by a fusion of
Pipermail (Mailman edition) and