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

[David Greenaway]

Hi all,

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.

A summary of the patches is as follows:

  [PATCH 1 of 3] pretty: Add ScalaDoc comments to "Pure/General/pretty.scala"

    Adds ScalaDoc comments to the "pretty.scala" file. I found that
    I had a hard time understanding what was going on. Hopefully these
    comments will assist future users and developers get up to speed
    a little faster.

  [PATCH 2 of 3] pretty: Ensure we are consistent in our use of space-widths versus character-widths

    Modifies "pretty.scala" to use the width of a space character
    (instead of an approximation of the width of an average character)
    when calculating how wide a string of spaces is.

    More details are in the patch comment.

  [PATCH 3 of 3] pretty: Use a more accurate method of measuring string lengths

    Use "Font.getStringBounds" instead of "FontMetrics.stringWidth" to
    measure string widths. The two calls give different values, and the
    former is the one actually used when performing rendering, and hence
    should be more accurate.

    Again, more details are in the patch comment.

I would appreciate it if Isabelle experts could review these patches
and, if acceptable, apply to mainline. The patches are based off
revision "60472a1b4536", the tip of the Isabelle repo at time of
writing.

If these patches are acceptable, I would also propose a few more changes
which I would be willing to draft:

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

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

Thoughts about these proposed patches would also be appreciated.


________________________________

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.