1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:45:26 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:53:00 2010 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5    private val document_0 = session.begin_document(buffer.getName)
     1.6  
     1.7 -  private val change_0 = new Change(document_0.id, None, Nil, Future.value(document_0, Nil))
     1.8 +  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
     1.9    private var _changes = List(change_0)   // owned by Swing thread
    1.10    def changes = _changes
    1.11    private var current_change = change_0
    1.12 @@ -76,7 +76,7 @@
    1.13          val old_doc = change1.document
    1.14          Document.text_edits(session, old_doc, new_id, eds)
    1.15        }
    1.16 -      val change2 = new Change(new_id, Some(change1), eds, result)
    1.17 +      val change2 = new Change(Some(change1), eds, result)
    1.18        _changes ::= change2
    1.19        session.input(change2)
    1.20        current_change = change2
    1.21 @@ -119,7 +119,7 @@
    1.22    /* transforming offsets */
    1.23  
    1.24    private def changes_from(doc: Document): List[Edit] =
    1.25 -    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
    1.26 +    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
    1.27        edits.toList
    1.28  
    1.29    def from_current(doc: Document, offset: Int): Int =

     2.1 --- a/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 21:45:26 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 21:53:00 2010 +0100
     2.3 @@ -40,7 +40,6 @@
     2.4  
     2.5  
     2.6  class Change(
     2.7 -  val id: Isar_Document.Document_ID,
     2.8    val parent: Option[Change],
     2.9    val edits: List[Edit],
    2.10    val result: Future[Document.Result])