tuned signature;

--- a/src/Pure/General/pretty.scala	Sun Mar 24 16:19:54 2013 +0100
+++ b/src/Pure/General/pretty.scala	Mon Mar 25 10:37:38 2013 +0100
@@ -31,14 +31,12 @@
   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
   }
 

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Mar 24 16:19:54 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Mar 25 10:37:38 2013 +0100
@@ -168,7 +168,7 @@
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
-    val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
+    val metric = pretty_metric(text_area.getPainter)
     val char_width = (metric.unit * metric.average).round.toInt
 
     val buffer = text_area.getBuffer
@@ -208,14 +208,19 @@
 
   /* pretty text metric */
 
-  def string_width(painter: TextAreaPainter, s: String): Double =
-    painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+  abstract class Pretty_Metric extends Pretty.Metric
+  {
+    def average: Double
+  }
 
-  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
+  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
+    new Pretty_Metric {
+      def string_width(s: String): Double =
+        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+
+      val unit = string_width(Pretty.space)
+      val average = string_width("mix") / (3 * unit)
+      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }
 }