# HG changeset patch
# User wenzelm
# Date 1413623974 -7200
# Node ID e46afcceb78159c1054ddb84eaba0b3529458de9
# Parent  1be9855fb579791e85bab41b9b79ac27856f8d98
tuned signature;

diff -r 1be9855fb579 -r e46afcceb781 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Oct 18 10:50:40 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Oct 18 11:19:34 2014 +0200
@@ -153,8 +153,16 @@
 
   private val context_rules = new ParserRuleSet("bibtex", "MAIN")
 
-  private class Line_Context(context: Option[Bibtex.Line_Context])
-    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
+  private class Line_Context(val context: Option[Bibtex.Line_Context])
+    extends TokenMarker.LineContext(context_rules, null)
+  {
+    override def hashCode: Int = context.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Line_Context => context == other.context
+        case _ => false
+      }
+  }
 
 
   /* token marker */
diff -r 1be9855fb579 -r e46afcceb781 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 10:50:40 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 11:19:34 2014 +0200
@@ -175,43 +175,40 @@
 
   /* line context */
 
-  class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C])
-    extends TokenMarker.LineContext(rules, null)
+  private val context_rules = new ParserRuleSet("isabelle", "MAIN")
+
+  class Line_Context(
+      val context: Option[Scan.Line_Context],
+      val structure: Outer_Syntax.Line_Structure)
+    extends TokenMarker.LineContext(context_rules, null)
   {
-    override def hashCode: Int = context.hashCode
+    override def hashCode: Int = (context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Generic_Line_Context[_] => context == other.context
+        case other: Line_Context => context == other.context && structure == other.structure
         case _ => false
       }
   }
 
-  def buffer_line_context[C](buffer: JEditBuffer, line: Int): Option[Generic_Line_Context[C]] =
+  def buffer_line_context(buffer: JEditBuffer, line: Int): Option[Line_Context] =
     Untyped.get(buffer, "lineMgr") match {
       case line_mgr: LineManager =>
         line_mgr.getLineContext(line) match {
-          case c: Generic_Line_Context[C] => Some(c)
+          case c: Line_Context => Some(c)
           case _ => None
         }
       case _ => None
     }
 
+  def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
+    buffer_line_context(buffer, line) match {
+      case Some(c) => c.structure
+      case _ => Outer_Syntax.Line_Structure.init
+    }
+
 
   /* token marker */
 
-  private val context_rules = new ParserRuleSet("isabelle", "MAIN")
-
-  private class Line_Context(
-      context: Option[Scan.Line_Context],
-      val structure: Outer_Syntax.Line_Structure)
-    extends Generic_Line_Context[Scan.Line_Context](context_rules, context)
-
-  def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
-    buffer_line_context[Scan.Line_Context](buffer, line) match {
-      case Some(c: Line_Context) => c.structure
-      case _ => Outer_Syntax.Line_Structure.init
-    }
-
   class Marker(mode: String) extends TokenMarker
   {
     override def markTokens(context: TokenMarker.LineContext,