[isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
david.greenaway at nicta.com.au
Thu Mar 21 07:14:06 CET 2013
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
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
* "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
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.
More information about the isabelle-dev