# HG changeset patch
# User wenzelm
# Date 1262379180 -3600
# Node ID 69852bd3c4c43fc0c6e45dacaed1a11b673d6cd4
# Parent  6b38fc0b34060057c6772395e2cbe57653ed389b
tuned Change: eliminated redundant copy of document id;

diff -r 6b38fc0b3406 -r 69852bd3c4c4 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:45:26 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:53:00 2010 +0100
@@ -60,7 +60,7 @@
 
   private val document_0 = session.begin_document(buffer.getName)
 
-  private val change_0 = new Change(document_0.id, None, Nil, Future.value(document_0, Nil))
+  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
   private var _changes = List(change_0)   // owned by Swing thread
   def changes = _changes
   private var current_change = change_0
@@ -76,7 +76,7 @@
         val old_doc = change1.document
         Document.text_edits(session, old_doc, new_id, eds)
       }
-      val change2 = new Change(new_id, Some(change1), eds, result)
+      val change2 = new Change(Some(change1), eds, result)
       _changes ::= change2
       session.input(change2)
       current_change = change2
@@ -119,7 +119,7 @@
   /* transforming offsets */
 
   private def changes_from(doc: Document): List[Edit] =
-    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
+    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
       edits.toList
 
   def from_current(doc: Document, offset: Int): Int =
diff -r 6b38fc0b3406 -r 69852bd3c4c4 src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 21:45:26 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 21:53:00 2010 +0100
@@ -40,7 +40,6 @@
 
 
 class Change(
-  val id: Isar_Document.Document_ID,
   val parent: Option[Change],
   val edits: List[Edit],
   val result: Future[Document.Result])