# HG changeset patch
# User wenzelm
# Date 1308403925 -7200
# Node ID a1db9a251a03a5d84375554355d1da7f3815d4ed
# Parent  e5dbf67b2a723a3471cc1c4d70215906cb369191
tuned signature;

diff -r e5dbf67b2a72 -r a1db9a251a03 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 15:18:57 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 15:32:05 2011 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
 import javax.swing.text.Segment
 
 
@@ -18,7 +18,7 @@
 {
   /* extended jEdit syntax styles */
 
-  private val plain_range: Int = JToken.ID_COUNT
+  private val plain_range: Int = JEditToken.ID_COUNT
   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
 
   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
@@ -62,7 +62,7 @@
           handler.handleToken(line, style, offset, length, context1)
           offset += length
         }
-        handler.handleToken(line, JToken.END, line.count, 0, context1)
+        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
 
         val context2 = context1.intern
         handler.setLineContext(context2)