# HG changeset patch
# User wenzelm
# Date 1308388923 -7200
# Node ID 095f90f8dca3decdcec03825bb8c6c03c221e852
# Parent  b41dea5772c6c1fcb4eec0c62023ff6258880631
simplified Line_Context (again);

diff -r b41dea5772c6 -r 095f90f8dca3 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 00:05:29 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 11:22:03 2011 +0200
@@ -30,8 +30,8 @@
 
   private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
 
-  private class Line_Context(val context: Scan.Context, prev: Line_Context)
-    extends TokenMarker.LineContext(isabelle_rules, prev)
+  private class Line_Context(val context: Scan.Context)
+    extends TokenMarker.LineContext(isabelle_rules, null)
   {
     override def hashCode: Int = context.hashCode
     override def equals(that: Any): Boolean =
@@ -43,16 +43,17 @@
 
   def token_marker(session: Session, buffer: Buffer): TokenMarker =
     new TokenMarker {
-      override def markTokens(raw_context: TokenMarker.LineContext,
+      override def markTokens(context: TokenMarker.LineContext,
           handler: TokenHandler, line: Segment): TokenMarker.LineContext =
       {
         val syntax = session.current_syntax()
-
-        val context = raw_context.asInstanceOf[Line_Context]
-        val ctxt = if (context == null) Scan.Finished else context.context
-
+        val ctxt =
+          context match {
+            case c: Line_Context => c.context
+            case _ => Scan.Finished
+          }
         val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
-        val context1 = new Line_Context(ctxt1, context)
+        val context1 = new Line_Context(ctxt1)
 
         var offset = 0
         for (token <- tokens) {