more uniform Pretty.char_width;

--- a/src/Pure/General/pretty.scala	Sat Jan 12 18:13:28 2013 +0100
+++ b/src/Pure/General/pretty.scala	Sat Jan 12 19:53:24 2013 +0100
@@ -14,7 +14,6 @@
 {
   /* spaces */
 
-  val spc = ' '
   val space = " "
 
   private val static_spaces = space * 4000
@@ -84,10 +83,13 @@
   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 font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
     else {
-      val unit = metrics.charWidth(spc).toDouble
+      val unit = char_width(metrics)
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 18:13:28 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 12 19:53:24 2013 +0100
@@ -160,17 +160,6 @@
   }
 
 
-  /* char width */
-
-  def char_width(text_area: TextArea): Int =
-  {
-    val painter = text_area.getPainter
-    val font = painter.getFont
-    val font_context = painter.getFontRenderContext
-    font.getStringBounds(" ", font_context).getWidth.round.toInt
-  }
-
-
   /* graphics range */
 
   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
@@ -179,6 +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_int(text_area.getPainter.getFontMetrics)
+
     val buffer = text_area.getBuffer
 
     val p = text_area.offsetToXY(range.start)
@@ -186,9 +177,9 @@
     val end = buffer.getLength
     val stop = range.stop
     val (q, r) =
-      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
+      if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
-        (text_area.offsetToXY(stop - 1), char_width(text_area))
+        (text_area.offsetToXY(stop - 1), char_width)
       else (text_area.offsetToXY(stop), 0)
 
     if (p != null && q != null && p.x < q.x + r && p.y == q.y)

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 12 18:13:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jan 12 19:53:24 2013 +0100
@@ -107,13 +107,12 @@
 
       getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
 
-      val font_metrics = getPainter.getFontMetrics(font)
-      val margin =
-        ((getWidth - getGutter.getWidth) / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
+      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(font_metrics))
+      val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(fm))
 
       future_rendering.map(_.cancel(true))
       future_rendering = Some(default_thread_pool.submit(() =>

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 12 18:13:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jan 12 19:53:24 2013 +0100
@@ -96,17 +96,15 @@
   val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
 
   {
-    val font_metrics = pretty_text_area.getPainter.getFontMetrics
+    val fm = pretty_text_area.getPainter.getFontMetrics
     val margin = rendering.tooltip_margin
     val lines =
-      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
+      XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
         (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
     val bounds = rendering.tooltip_bounds
-    val w =
-      (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
-    val h =
-      (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
+    val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt
+    val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
     pretty_text_area.setPreferredSize(new Dimension(w, h))
     window.pack
 

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jan 12 18:13:28 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jan 12 19:53:24 2013 +0100
@@ -490,7 +490,7 @@
             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, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
+            gfx.drawRect(x, y, Pretty.char_width_int(fm) - 1, fm.getHeight - 1)
           }
         }
       }