# HG changeset patch
# User wenzelm
# Date 1363881494 -3600
# Node ID a981a5c8a505f895fdae2b9ae83a42532b730a18
# Parent  18120e26f8187fd059eaeda806f3162e8fe0bad0
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;

diff -r 18120e26f818 -r a981a5c8a505 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 21 16:35:53 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 21 16:58:14 2013 +0100
@@ -72,14 +72,6 @@
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
-  private 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 = string(spaces(wd), wd.toDouble)
-    def content: XML.Body = tx.reverse
-  }
-
   private val margin_default = 76
   private def metric_default(s: String) = s.length.toDouble
 
@@ -95,6 +87,18 @@
   def formatted(input: XML.Body, margin: Int = margin_default,
     metric: String => Double = 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 content: XML.Body = tx.reverse
+    }
+
     val breakgain = margin / 20
     val emergencypos = margin / 2