# HG changeset patch
# User wenzelm
# Date 1263214532 -3600
# Node ID 309d545295d36a314c39ba21c100f3b5caadb573
# Parent  847c00f5535a92630c74bc3fc674c418a3a667c4
eliminated obsolete isabelle.proofdocument.Token;

diff -r 847c00f5535a -r 309d545295d3 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 12:17:47 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 13:55:32 2010 +0100
@@ -11,8 +11,7 @@
 import isabelle.Markup
 
 import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token => JToken,
-  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
+import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
 
 import java.awt.Color
 import java.awt.Font
@@ -33,7 +32,7 @@
 
   private val choose_byte: Map[String, Byte] =
   {
-    import JToken._
+    import Token._
     Map[String, Byte](
       // logical entities
       Markup.TCLASS -> LABEL,
@@ -139,7 +138,7 @@
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
 
-    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
+    handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
     handler.setLineContext(context)
     context
   }
diff -r 847c00f5535a -r 309d545295d3 src/Tools/jEdit/src/proofdocument/token.scala
--- a/src/Tools/jEdit/src/proofdocument/token.scala	Mon Jan 11 12:17:47 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-/*
- * Document tokens as text ranges
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-
-object Token {
-  object Kind extends Enumeration
-  {
-    val COMMAND_START = Value("COMMAND_START")
-    val COMMENT = Value("COMMENT")
-    val OTHER = Value("OTHER")
-  }
-
-  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
-    def stop(t: Token) = starts(t) + t.length
-    tokens match {
-      case Nil => ""
-      case tok :: toks =>
-        val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
-          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
-        res
-    }
-  }
-
-}
-
-class Token(
-  val content: String,
-  val kind: Token.Kind.Value)
-{
-  override def toString = content
-  val length = content.length
-  val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
-}