use RichString.* to produce blanks;

--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 21:27:51 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 21:36:22 2009 +0200
@@ -18,18 +18,13 @@
     val OTHER = Value("OTHER")
   }
 
-  private def fill(n: Int) = {
-    val blanks = new Array[Char](n)
-    for(i <- 0 to n - 1) blanks(i) = ' '
-    new String(blanks)
-  }
   def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = {
     def stop(t: Token) = starts(t) + t.length
     tokens match {
       case Nil => ""
       case t::tokens => ( tokens.foldLeft
           (t.content, stop(t))
-          ((a, token) => (a._1 + fill(starts(token) - a._2) + token.content, stop(token)))
+          ((a, token) => (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
         )._1
     }
   }