1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 12:17:47 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Mon Jan 11 13:55:32 2010 +0100
     1.3 @@ -11,8 +11,7 @@
     1.4  import isabelle.Markup
     1.5  
     1.6  import org.gjt.sp.jedit.buffer.JEditBuffer
     1.7 -import org.gjt.sp.jedit.syntax.{Token => JToken,
     1.8 -  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
     1.9 +import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
    1.10  
    1.11  import java.awt.Color
    1.12  import java.awt.Font
    1.13 @@ -33,7 +32,7 @@
    1.14  
    1.15    private val choose_byte: Map[String, Byte] =
    1.16    {
    1.17 -    import JToken._
    1.18 +    import Token._
    1.19      Map[String, Byte](
    1.20        // logical entities
    1.21        Markup.TCLASS -> LABEL,
    1.22 @@ -139,7 +138,7 @@
    1.23      if (next_x < stop)
    1.24        handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
    1.25  
    1.26 -    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
    1.27 +    handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
    1.28      handler.setLineContext(context)
    1.29      context
    1.30    }

     2.1 --- a/src/Tools/jEdit/src/proofdocument/token.scala	Mon Jan 11 12:17:47 2010 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,39 +0,0 @@
     2.4 -/*
     2.5 - * Document tokens as text ranges
     2.6 - *
     2.7 - * @author Johannes Hölzl, TU Munich
     2.8 - * @author Fabian Immler, TU Munich
     2.9 - */
    2.10 -
    2.11 -package isabelle.proofdocument
    2.12 -
    2.13 -
    2.14 -object Token {
    2.15 -  object Kind extends Enumeration
    2.16 -  {
    2.17 -    val COMMAND_START = Value("COMMAND_START")
    2.18 -    val COMMENT = Value("COMMENT")
    2.19 -    val OTHER = Value("OTHER")
    2.20 -  }
    2.21 -
    2.22 -  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
    2.23 -    def stop(t: Token) = starts(t) + t.length
    2.24 -    tokens match {
    2.25 -      case Nil => ""
    2.26 -      case tok :: toks =>
    2.27 -        val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
    2.28 -          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
    2.29 -        res
    2.30 -    }
    2.31 -  }
    2.32 -
    2.33 -}
    2.34 -
    2.35 -class Token(
    2.36 -  val content: String,
    2.37 -  val kind: Token.Kind.Value)
    2.38 -{
    2.39 -  override def toString = content
    2.40 -  val length = content.length
    2.41 -  val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
    2.42 -}