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

[David Greenaway]

On 22/03/13 02:13, Makarius wrote:
> On Thu, 21 Mar 2013, David Greenaway wrote:
>
>> Attached is a patch series which attempts to improve the font rendering
>> in the Isabelle/jEdit output window. In particular, it attempts to
>> reduce the number of cases where text is inadvertently rendered off the
>> right-hand-side of the output window, requiring the user to scroll
>> across to see the last few characters.
>
> There seem to be one or two important details that you have found out
> about Java text measuring and rendering, but they are difficult to
> spot in the mass of changes.

I tried my best to ensure that each patch made only a single change, and
each such change was well documented in the patch header. Let me try
being more succinct:

  PATCH 1: Document "pretty.scala", so future developers require less
           time to understand what is going on.

  PATCH 2: When determining how long a string of spaces is, use
           'width(" ") * n' instead of 'width("mix") * n / 3'.

  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.

> Also note that chapter 0 of the "implementation" manual and
> README_REPOSITORY give some general explanations how Isabelle sources
> and changes over sources usually look like.  You cannot just define
> your personal preferred style how things should be done and expect
> that it is accepted.  (If it would, the Isabelle sources would be
> a huge chaos.)

Again, I tried my best to conform to Chapter 0, README_REPOSITORY, the
existing Scala code style and the ScalaDoc style guides [1]. If you
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

>>  * "pretty.scala" currently uses "space-widths" as its internal unit.
>>    It may be beneficial to refactor this to use an arbitrary unit
>>    internally (chosen by the caller) and measure the space strings it
>>    generates (also updating "pretty.ML" to match). This would prevent
>>    the current dance of needing to divide out the width of a space
>>    everywhere.
>
> Can you say more directly what you think that is actually wrong?  As
> long as rounding is done properly (which is not necessarily the case)
> any unit should work.  Java also uses floating point in some
> interfaces, while integer pixels in other spots.  Both can lead to
> problems, but I prefer to delegate calculations to floating point
> arithmetic if possible.

"pretty.scala" has no need to know what units it is working in. It
should just use the provided measure function to calculate string
widths. This would mean the callers can use the most convenient
representation for them; presumably pixels for callers who will be
rendering to the screen, and "number of characters" for those working in
ASCII.

Also I am not suggesting moving away from floating point. In particular,
the brave new world of sub-pixel font rendering would still require
this.

>>  * "Rich_Text_Area.print_valid_line" and
>>    "TextAreaPainter.PaintText.paintValidLine" use two different text
>>    rendering techniques. The current implementation of "Rich_Text_Area"
>>    uses the former to paint text, while the latter to calculate the
>>    width of the painted text. This means that a horizontal scrollbar
>>    may be enabled when no actual text overflows the right hand side of
>>    the screen.
>>
>>    We should probably do our own width calculations instead of calling
>>    jEdit to paint the text a second time. (It is probably also worth
>>    inspecting the implementation of "PaintText.paintValidLine" to
>>    determine if their font-rendering method choices are preferable).
>>
>>  * Markup.SEPARATOR, as far as I can tell, is currently ignored when
>>    rendering text. It would be nice to have some sort of visual
>>    indicator between different blocks of text. For example, in the
>>    output of "find_theorems", it is hard to determine when one theorem
>>    ends and another starts.
>>
>>    Ideally, a small vertical gap could be rendered between different
>>    blocks. This may be hard in jEdit, which might assume that all lines
>>    are of the same height. An alternative would be to have a subtle
>>    visual marker, such as a faint line between different blocks.
>>
>>  * The jEdit "subpixel text rendering" option is currently ignored by
>>    Rich_Text_Area. It would be nice to add support for this, which may
>>    require some rethinking of how the cursor rendering code works.
>
> All of that refers to particulars of the jEdit text rendering model.
> I am struggling with that for several years already, and the quality
> is already much better than anything I've seen before or elsewhere.
>
> Before doing greater changes in any of these respects, one needs to
> revisit carefully what I've done already (including study of the relevant
> changesets, which usually document that), and also get involved with the
> jEdit project itself.  The latter is not easy -- I've just required 2-3
> weeks to get a rather trivial patch accepted.

I would imagine it must be quite frustrating when upstream maintainers
refuse to accept community contributions.

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.