# HG changeset patch
# User wenzelm
# Date 1283108562 -7200
# Node ID 23513fb32e7bc75345bf8437f10b0667198951cf
# Parent  227dd9a9459a54b58b523db34ae61b284df1701b
Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;

diff -r 227dd9a9459a -r 23513fb32e7b src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 29 20:09:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 29 21:02:42 2010 +0200
@@ -57,9 +57,18 @@
 
     /* line context */
 
-    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
-    class LineContext(val line: Int, prev: LineContext)
-      extends TokenMarker.LineContext(rule_set, prev)
+    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
+
+    class Line_Context(val line: Int, prev: Line_Context)
+      extends TokenMarker.LineContext(dummy_rules, prev)
+    {
+      override def hashCode: Int = line
+      override def equals(that: Any) =
+        that match {
+          case other: Line_Context => line == other.line
+          case _ => false
+        }
+    }
 
 
     /* mapping to jEdit token types */
@@ -259,9 +268,9 @@
       Isabelle.swing_buffer_lock(buffer) {
         val snapshot = Document_Model.this.snapshot()
 
-        val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
+        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
         val line = if (prev == null) 0 else previous.line + 1
-        val context = new Document_Model.Token_Markup.LineContext(line, previous)
+        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
 
         val start = buffer.getLineStartOffset(line)
         val stop = start + line_segment.count