# HG changeset patch
# User wenzelm
# Date 1276463049 -7200
# Node ID d66e6cc47fab982481d3c4518ab2d82d2338adde
# Parent  25078ba4443643c8143d279fd703e4dc617aa099
Pretty.string_of (in Scala): actually observe margin/metric;

diff -r 25078ba44436 -r d66e6cc47fab src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Jun 13 22:33:18 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sun Jun 13 23:04:09 2010 +0200
@@ -134,7 +134,7 @@
 
   def string_of(input: List[XML.Tree], margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    formatted(input).iterator.flatMap(XML.content).mkString
+    formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
 
 
   /* unformatted output */