Re: [isabelle] word wrapping in jEdit output panel



On 14/03/13 00:52, Makarius wrote:
> On Wed, 13 Mar 2013, John Wickerson wrote:
>> The word wrapping in the Output window of Isabelle/jEdit is a little
>> bit off. That is, each line of text breaks about 1cm beyond the
>> right-hand edge of the Output window (and that's independent of how
>> I resize the window). Of course it's only a minor quibble because
>> I can always scroll horizontally a little bit to see the rest of the
>> output. It doesn't help to turn on/off the gutter.

I also hit this problem, and had a go at fixing, with only minor
success.

> I think you mean the breaking of pretty-printed formal output.
> (Word-wrap in the source is a different issue: there is also a snag
> here, because Isabelle tokenization for {* ... *} is in conflict with
> jEdit tokenization for words.)
>
> The font metrics and window size parameters for pretty printed output
> are only precise once the inner GUI component geometry is known.  It
> does not quite work with extra decoration (scrollbars, window
> borders): before the window is mapped these sizes are unknown, or
> I did not know how to get them in Java/AWT/Swing.

I found that "getPainter.getWidth" gave a better indication of a window
size as opposed to getting the control's width and attempting to
subtract off the size of scrollbars, etc.

Another snag I hit is that "metrics.stringWidth" doesn't take into
account anti-aliasing, which after 80 characters of rendering really
starts to add up.

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

Cheers,
David


________________________________

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
description:
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. Despite this, the goal is still two
characters plus a few pixels out, which will require further investigation.


diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala
+++ b/src/Pure/General/pretty.scala
@@ -8,6 +8,7 @@
 
 
 import java.awt.FontMetrics
+import java.awt.font.FontRenderContext
 
 
 object Pretty
@@ -83,8 +84,14 @@
   private val margin_default = 76
   private def metric_default(s: String) = s.length.toDouble
 
-  def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3
-  def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt
+  def char_width(metrics: FontMetrics): Double =
+  {
+    val test_string = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ 0123456789!?. "
+    val render_context = new FontRenderContext(metrics.getFont.getTransform, true, true)
+    metrics.getFont.getStringBounds(test_string, render_context).getWidth / test_string.length
+  }
+
+  def char_width_int(metrics: FontMetrics): Int = char_width(metrics).ceil.toInt
 
   def font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
diff --git a/src/Tools/jEdit/src/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala
+++ b/src/Tools/jEdit/src/pretty_text_area.scala
@@ -109,11 +109,14 @@
       getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
 
       val fm = getPainter.getFontMetrics
-      val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
+      val num_visible_characters = ((getPainter.getWidth
+              / (Pretty.char_width(fm) max 1.0)).floor.toInt) 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))
+
+      val formatted_body = Pretty.formatted(current_body,
+              num_visible_characters - 2, Pretty.font_metric(fm))
 
       future_rendering.map(_.cancel(true))
       future_rendering = Some(default_thread_pool.submit(() =>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.