# HG changeset patch
# User wenzelm
# Date 1273612189 -7200
# Node ID da7628b3d231742fb971f5be1758a7846b1f0e8a
# Parent  fc672bf92fc2d7d2161caf04aacd3da8c208a77c
predefined spaces;

diff -r fc672bf92fc2 -r da7628b3d231 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue May 11 17:55:19 2010 +0200
+++ b/src/Pure/General/symbol.scala	Tue May 11 23:09:49 2010 +0200
@@ -15,13 +15,16 @@
 {
   /* spaces */
 
-  private val static_spaces = " " * 4000
+  val spc = ' '
+  val space = " "
+
+  private val static_spaces = space * 4000
 
   def spaces(k: Int): String =
   {
     require(k >= 0)
     if (k < static_spaces.length) static_spaces.substring(0, k)
-    else " " * k
+    else space * k
   }
 
 
@@ -278,7 +281,7 @@
       "\\<^isub>", "\\<^isup>")
 
     private val blanks =
-      Decode_Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+      Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
 
     private val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")