--- 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
}