Re: [isabelle] word wrapping in jEdit output panel
On 14/03/13 10:00, David Greenaway wrote:
> I also hit this problem, and had a go at fixing, with only minor
> Attached is a patch that may be a starting point to address some of
> the problems, but is by no means complete. I still get overflows when
> Isabelle renders many wide characters on a line.
> I suspect a "proper" solution is to give the line-breaking algorithm
> a better understanding of how wide each character is, but I haven't
> had a chance to sit down and work out how hard this would be to
I decided to sit down and actually see if I could come up with a better
solution for this problem. Attached is what I came up with (replacing
my previously posted patch completely).
In particular, "Pretty" internally uses "number of spaces" as its
measuring units. This patch attempts modifies "PrettyTextArea" to more
accurately measure strings and feed these widths into "Pretty" in the
This seems to give good results on Linux, with all combinations of
hinted/non-hinted aliased/anti-aliased fixed-width/non-fixed-width fonts
A one-space margin remains on the right-hand-side because non-hinted
+ anti-aliased fonts still sometimes overflows by a few pixels, and
I couldn't determine why.
The patch doesn't attempt to fix SideKick or tool-tips; if the Isabelle
maintainers are happy with the approach in this patch, I would be happy
to extend it.
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.
user: David Greenaway <david.greenaway at nicta.com.au>
date: Tue Feb 26 12:24:14 2013 +1100
jedit: Fix subgoal rendering to avoid inadvertantly rendering goals off the side of the display.
We attempt to use the correct width of the text area and a higher-fidelity
measurement on font character widths.
diff --git a/src/Tools/jEdit/src/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala
@@ -108,12 +108,26 @@
- val fm = getPainter.getFontMetrics
- val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
- val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(fm))
+ /* Measure the rendered width of a string in pixels. */
+ val fontMetrics = getPainter.getFontMetrics
+ val measureString = ((s : String) =>
+ fontMetrics.getFont.getStringBounds(s, getPainter.getFontRenderContext).getWidth)
+ /* Measure the rendered width of a string as a multiple of the width of
+ * a single "space" character. */
+ val spaceWidth = measureString(" ")
+ val stringSpacesWidth = ((s : String) => measureString(s) / spaceWidth)
+ /* Calculate the size of our canvas, in terms of number of space characters
+ * that fit within it. */
+ val textAreaSpacesWidth =
+ ((getPainter.getWidth.toDouble / spaceWidth).floor.toInt - 1) max 20
+ val formatted_body = Pretty.formatted(current_body,
+ textAreaSpacesWidth, stringSpacesWidth)
future_rendering = Some(default_thread_pool.submit(() =>
This archive was generated by a fusion of
Pipermail (Mailman edition) and