On Mon, 25 Mar 2013, David Greenaway wrote:
On 22/03/13 22:48, Makarius wrote:
On Fri, 22 Mar 2013, David Greenaway wrote:
PATCH 3: When measuring strings, use "Font.getStringBounds" instead
of "FontMetrics.stringWidth". The latter doesn't take into
account anti-aliasing or kerning, while the former is what
is actually used when rendering the strings to the screen.
That seems to be the most important point here. It requires some further
investigation how jEdit measures things in general, so see if it agrees
with the actual painting. There might be some deeper problem of
Graphics2D painting vs. font metrics here, that needs to be investigated.
If you can tell more, pointing to sources by the jEdit guys or Oracle, I
will listen attentively.
The problem that this patch fixes is internal to the Isabelle sources,
and not directly related to how jEdit measures strings. As mentioned
above, Pretty uses "FontMetrics.stringWidth" to determine if text will
overflow, while "Rich_Text_Area" actually uses "Font.getStringBounds" to
layout text. Because the two values disagree for the same strings, we
get inadvertant overflow to the right.
I've come across that part of jEdit and Isabelle/Scala sources again
(presenty at Isabelle/193ba70666bd). My impression is that
FontMetrics.stringWidth and FontMetrics.getStringBounds merely differ in
the result type: Int vs. Double. I also hope that
FontMetrics.getStringBounds and Font.getStringBounds are the same, if
provided by suitable parameters, but there is no problem to use the latter
uniformly.
It seems that Java 2D text is normally snapped on a pixel grid, unless you
explicitly ask for "fractional font metrics" as rendering hint. This is
off by default, and normally degrades rendering quality. (Did you have
that enabled? Did it actually improve visual appearance? On which
physical display?)
What is also funny is that the idea of "avarage char width" that I've got
wrong in the first attempt is also a bit confused in the jEdit sources
(hidden behind misleading Javadocs and slightly outdated code), although
jEdit gets its visual tab width and preferred window geometry right in the
end, just due to the way how slightly confusing operations happen to be
used.
To improve general uniformity and potential of surprise, I've clarified
the Pretty.Metric and JEdit_Lib.Pretty_Metric notions once again, to make
more explicit what this is all about. It does not change the situation of
occasionaly scrollbars and 0.3 of a character off the vieport, though.
There must be other effects, about jEdit calculating scrollbar parameters.
Generally note, that the font metric business can never be 100% right --
not just because of floating point arithmetic. When text is actually
rendered, its font-style might change again in the tokenization. I don't
think this tiny snag deserves more of this undue priority right now.
(There are no bugs, no fixes, just continous improvements of
approximations, until perfection is reached in the limit.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
