# HG changeset patch
# User wenzelm
# Date 1273403542 -7200
# Node ID 096ebe74aeaf9e4b0bf04b50e38b41f5391b00e2
# Parent  40837a7b32a7c7aa5dc6793e6de3f9b6b56b5fb9
static Symbol.spaces;

diff -r 40837a7b32a7 -r 096ebe74aeaf src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat May 08 21:25:25 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sun May 09 13:12:22 2010 +0200
@@ -30,7 +30,8 @@
   object Break
   {
     def apply(width: Int): XML.Tree =
-      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width)))
+      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)),
+        List(XML.Text(Symbol.spaces(width))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
@@ -48,7 +49,7 @@
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0, nl = nl + 1)
     def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + s.length)
-    def blanks(wd: Int): Text = string(" " * wd)
+    def blanks(wd: Int): Text = string(Symbol.spaces(wd))
     def content: List[XML.Tree] = tx.reverse
   }
 
@@ -126,7 +127,7 @@
     def fmt(tree: XML.Tree): List[XML.Tree] =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
-        case Break(wd) => List(XML.Text(" " * wd))
+        case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
         case FBreak => List(XML.Text(" "))
         case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
diff -r 40837a7b32a7 -r 096ebe74aeaf src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat May 08 21:25:25 2010 +0200
+++ b/src/Pure/General/symbol.scala	Sun May 09 13:12:22 2010 +0200
@@ -13,6 +13,18 @@
 
 object Symbol
 {
+  /* spaces */
+
+  private val static_spaces = " " * 4000
+
+  def spaces(k: Int): String =
+  {
+    require(k >= 0)
+    if (k < static_spaces.length) static_spaces.substring(0, k)
+    else " " * k
+  }
+
+
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)