src/Pure/General/pretty.scala

 import java.awt.FontMetrics
 
 
 object Pretty
 {
+  /* spaces */
+
+  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 space * k
+  }
+
+
   /* markup trees with physical blocks and breaks */
 
   def block(body: XML.Body): XML.Tree = Block(2, body)
 
   object Block

 
   object Break
   {
     def apply(w: Int): XML.Tree =
       XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
-        List(XML.Text(Symbol.spaces(w))))
+        List(XML.Text(spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
         case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
         case _ => None

 
   private sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
-    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+    def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
     def content: XML.Body = tx.reverse
   }
 
   private val margin_default = 76
   private def metric_default(s: String) = s.length.toDouble
 
   def font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
     else {
-      val unit = metrics.charWidth(Symbol.spc).toDouble
+      val unit = metrics.charWidth(spc).toDouble
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 
   def formatted(input: XML.Body, margin: Int = margin_default,
     metric: String => Double = metric_default): XML.Body =

   def unformatted(input: XML.Body): XML.Body =
   {
     def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
-        case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
-        case FBreak => List(XML.Text(Symbol.space))
+        case Break(wd) => List(XML.Text(spaces(wd)))
+        case FBreak => List(XML.Text(space))
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
     input.flatMap(standard_format).flatMap(fmt)
   }