# HG changeset patch
# User wenzelm
# Date 1243971856 -7200
# Node ID 4c65620f53188344a307d02c4ffced7050d7d42e
# Parent  3457ef52de04568b3677f7c055d12cdcb48bac16
tuned;

diff -r 3457ef52de04 -r 4c65620f5318 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 21:36:22 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 21:44:16 2009 +0200
@@ -18,14 +18,14 @@
     val OTHER = Value("OTHER")
   }
 
-  def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = {
+  def string_from_tokens(tokens: List[Token], starts: 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 + " " * (starts(token) - a._2) + token.content, stop(token)))
-        )._1
+      case t :: tokens =>
+        val (res, _) = tokens.foldLeft(t.content, stop(t))((a, token) =>
+          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
+        res
     }
   }