# HG changeset patch
# User wenzelm
# Date 1364040759 -3600
# Node ID eaa1c4cc11068264bb1923305978ce1f0c882c59
# Parent  38a796ac4ab7cd16bc3d1db6d04d8dc093f9d80b
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

diff -r 38a796ac4ab7 -r eaa1c4cc1106 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Pure/General/pretty.scala	Sat Mar 23 13:12:39 2013 +0100
@@ -26,6 +26,23 @@
   }
 
 
+  /* text metric -- standardized to width of space */
+
+  abstract class Metric
+  {
+    val unit: Double
+    def average: Double
+    def apply(s: String): Double
+  }
+
+  object Metric_Default extends Metric
+  {
+    val unit = 1.0
+    val average = 1.0
+    def apply(s: String): Double = s.length.toDouble
+  }
+
+
   /* markup trees with physical blocks and breaks */
 
   def block(body: XML.Body): XML.Tree = Block(2, body)
@@ -73,29 +90,15 @@
     }
 
   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 font_metric(metrics: FontMetrics): String => Double =
-    if (metrics == null) ((s: String) => s.length.toDouble)
-    else {
-      val unit = char_width(metrics)
-      ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
-    }
 
   def formatted(input: XML.Body, margin: Int = margin_default,
-    metric: String => Double = metric_default): XML.Body =
+    metric: Metric = Metric_Default): XML.Body =
   {
     sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
     {
       def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
-      def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
-      def blanks(wd: Int): Text =
-      {
-        val s = spaces(wd)
-        string(s, metric(s))
-      }
+      def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
+      def blanks(wd: Int): Text = string(spaces(wd))
       def content: XML.Body = tx.reverse
     }
 
@@ -153,14 +156,14 @@
           val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
           format(ts1, blockin, after, btext1)
 
-        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
+        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
       }
 
     format(standard_format(input), 0.0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Int = margin_default,
-      metric: String => Double = metric_default): String =
+      metric: Metric = Metric_Default): String =
     XML.content(formatted(input, margin, metric))
 
 
diff -r 38a796ac4ab7 -r eaa1c4cc1106 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 13:12:39 2013 +0100
@@ -15,7 +15,7 @@
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
 
 object JEdit_Lib
@@ -168,7 +168,8 @@
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
-    val char_width = Pretty.char_width(text_area.getPainter.getFontMetrics).round.toInt
+    val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
+    val char_width = (metric.unit * metric.average).round.toInt
 
     val buffer = text_area.getBuffer
 
@@ -203,5 +204,18 @@
       case _ => None
     }
   }
+
+
+  /* pretty text metric */
+
+  def string_width(painter: TextAreaPainter, s: String): Double =
+    painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+
+  def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
+    new Pretty.Metric {
+      val unit = string_width(painter, Pretty.space)
+      val average = string_width(painter, "mix") / (3 * unit)
+      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit
+    }
 }
 
diff -r 38a796ac4ab7 -r eaa1c4cc1106 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 13:12:39 2013 +0100
@@ -108,12 +108,12 @@
     getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
 
     if (getWidth > 0) {
-      val fm = getPainter.getFontMetrics
-      val margin = (getPainter.getWidth / (Pretty.char_width(fm).ceil.toInt max 1)) max 20
+      val metric = JEdit_Lib.pretty_metric(getPainter)
+      val margin = (getPainter.getWidth.toDouble / metric.unit).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, margin, metric)
 
       future_rendering.map(_.cancel(true))
       future_rendering = Some(default_thread_pool.submit(() =>
diff -r 38a796ac4ab7 -r eaa1c4cc1106 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 13:12:39 2013 +0100
@@ -190,10 +190,10 @@
 
     {
       val painter = pretty_text_area.getPainter
-      val fm = painter.getFontMetrics
-      val margin = rendering.tooltip_margin
+      val metric = JEdit_Lib.pretty_metric(painter)
+      val margin = (rendering.tooltip_margin * metric.average).toInt
       val lines =
-        XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
+        XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
       if (window.getWidth == 0) {
@@ -208,10 +208,10 @@
 
       val bounds = rendering.tooltip_bounds
       val w =
-        ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+        ((metric.unit * (margin + 1)).round.toInt + deco_width) min
         (screen_bounds.width * bounds).toInt
       val h =
-        (fm.getHeight * (lines + 1) + deco_height) min
+        (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
         (screen_bounds.height * bounds).toInt
 
       window.setSize(new Dimension(w, h))
diff -r 38a796ac4ab7 -r eaa1c4cc1106 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 13:12:39 2013 +0100
@@ -497,11 +497,12 @@
           if (start <= caret && caret == end - 1) {
             val painter = text_area.getPainter
             val fm = painter.getFontMetrics
+            val metric = JEdit_Lib.pretty_metric(painter)
 
             val offset = caret - text_area.getLineStartOffset(physical_line)
             val x = text_area.offsetToXY(physical_line, offset).x
             gfx.setColor(painter.getCaretColor)
-            gfx.drawRect(x, y, Pretty.char_width(fm).round.toInt - 1, fm.getHeight - 1)
+            gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
           }
         }
       }