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

[David Greenaway]

On 26/03/13 00:40, Makarius wrote:
> On Mon, 25 Mar 2013, David Greenaway wrote:
[...]
>> 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).

That seems to have improved the situation significantly, thank you.

> 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?)

Font hinting tends to be a matter of personal preference. Some people
prefer that fonts are rendered snapped to the monitor's pixel grid so
everything looks sharp, while others (such as myself) prefer accurate
glyphs, even if it means fonts look a little "blurry". (A nice overview
of the different problems and possible solutions is at [1].)

  [1]: http://www.antigrain.com/research/font_rasterization/

> 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.

I'm still confused as to why everything needs to be normalised to the
width of a space, but in general the code seems to make more sense now.
Thanks for the changes.

> 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.)

Yes, I did notice that and understand that fixing this would require
deeper changes that not even I am motivated to investigate right now.

Now that the font rendering code has settled down again, should I update
and resubmit my documentation patches to "pretty.scala"? If so, would
you prefer ScalaDoc or just plain Scala comments?

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.