src/Pure/General/symbol.scala

 
 object Symbol
 {
   /* 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
   }
 
 
   /* Symbol regexps */
 

       "\\<Psi>", "\\<Omega>",
 
       "\\<^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("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
     def is_letter(sym: String): Boolean = letters.contains(sym)