# HG changeset patch
# User wenzelm
# Date 1243971382 -7200
# Node ID 3457ef52de04568b3677f7c055d12cdcb48bac16
# Parent  17c83413b7fe8fee3bf7d026da3748dc6cf6aec3
use RichString.* to produce blanks;

diff -r 17c83413b7fe -r 3457ef52de04 src/Tools/jEdit/src/proofdocument/Token.scala
--- 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
     }
   }