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)