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

[Makarius]

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.

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

The writing style of Isabelle/Scala is similar to Isabelle/ML, with a few 
modifications to accomodate Scala customs.  The coincidence with Java one 
the same JVM can be ignored for that purpose.


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


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


As a general principle, I am accepting non-trivial changesets to sources 
where I am responsible only as last resorts -- it has lead to subtle 
problems more than once in the past.

It is much quicker to explain briefly what you mean, and maybe accompany 
it by some examples and results of experiments, to point to the key 
issues.


 	Makarius