src/Pure/General/pretty.scala

--- 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)
     }