[isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.

[Makarius]

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