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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
