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

David Greenaway david.greenaway at nicta.com.au
Sun Mar 24 23:42:24 CET 2013

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 tried to explain this in the header of "Patch 3", along with
a suggested fix. Let me know if it doesn't make sense.

The differences between how jEdit renders text and how Isabelle renders
text cause a different problem (mentioned in my "proposed patches" list
in my original email). I haven't investigated this fully yet, because
I was waiting to determine what the outcome of this original patch
series was.

>> the ScalaDoc style guides [1]
>> could be a little more concrete on where I went wrong, I would be happy
>> to reformat the patches.
>>  [1]: http://docs.scala-lang.org/style/scaladoc.html
> This one does not apply to Isabelle/Scala sources.  ScalaDoc is no
> universal standard, and it does not lead to well-document sources. You can
> see the results of some decades of JavaDoc practice when you look through
> the main JDK sources, which I am occasionally forced to do.

Is your objection to to the particular comments I added in Patch 1? (If
so, do you have any suggestions as to how I could improve them?)

Or, do you just prefer to have plain comments instead of parsable ones?
(If so, I would be happy to adjust them, and re-submit the patch.)

> General Scala coding style is still an open question, and Isabelle/Scala
> has its own style inherited from Isabelle/ML.

No problem. Could you please point out where I went wrong, so I know
better for next time?



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.

More information about the isabelle-dev mailing list