1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 03 20:50:07 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 03 23:03:04 2010 +0100
     1.3 @@ -58,8 +58,10 @@
     1.4  {
     1.5    /* history */
     1.6  
     1.7 +  private val document_0 = session.begin_document(buffer.getName)
     1.8 +
     1.9    @volatile private var history =  // owned by Swing thread
    1.10 -    new Change(None, Nil, Future.value(session.begin_document(buffer.getName), Nil))
    1.11 +    new Change(None, Nil, document_0.id, Future.value(document_0, Nil))
    1.12  
    1.13    def current_change(): Change = history
    1.14  
    1.15 @@ -77,8 +79,8 @@
    1.16    private def changes_from(doc: Document): List[Edit] =
    1.17    {
    1.18      Swing_Thread.assert()
    1.19 -    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
    1.20 -      edits_buffer.toList
    1.21 +    (edits_buffer.toList /:
    1.22 +      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
    1.23    }
    1.24  
    1.25    def from_current(doc: Document, offset: Int): Int =
    1.26 @@ -103,10 +105,11 @@
    1.27      if (!edits_buffer.isEmpty) {
    1.28        val edits = edits_buffer.toList
    1.29        val change1 = current_change()
    1.30 +      val result_id = session.create_id()
    1.31        val result: Future[Document.Result] = Future.fork {
    1.32 -        Document.text_edits(session, change1.document, session.create_id(), edits)
    1.33 +        Document.text_edits(session, change1.document, result_id, edits)
    1.34        }
    1.35 -      val change2 = new Change(Some(change1), edits, result)
    1.36 +      val change2 = new Change(Some(change1), edits, result_id, result)
    1.37        history = change2
    1.38        result.map(_ => session.input(change2))
    1.39        edits_buffer.clear

     2.1 --- a/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 03 20:50:07 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 03 23:03:04 2010 +0100
     2.3 @@ -42,13 +42,19 @@
     2.4  class Change(
     2.5    val parent: Option[Change],
     2.6    val edits: List[Edit],
     2.7 +  val id: Isar_Document.Document_ID,
     2.8    val result: Future[Document.Result])
     2.9  {
    2.10 -  // FIXME iterator
    2.11 -  def ancestors(done: Change => Boolean): List[Change] =
    2.12 -    if (done(this)) Nil
    2.13 -    else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
    2.14 -  def ancestors: List[Change] = ancestors(_ => false)
    2.15 +  def ancestors: Iterator[Change] = new Iterator[Change]
    2.16 +  {
    2.17 +    private var state: Option[Change] = Some(Change.this)
    2.18 +    def hasNext = state.isDefined
    2.19 +    def next =
    2.20 +      state match {
    2.21 +        case Some(change) => state = change.parent; change
    2.22 +        case None => throw new NoSuchElementException("next on empty iterator")
    2.23 +      }
    2.24 +  }
    2.25  
    2.26    def document: Document = result.join._1
    2.27    def document_edits: List[Document.Structure_Edit] = result.join._2

     3.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 03 20:50:07 2010 +0100
     3.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 03 23:03:04 2010 +0100
     3.3 @@ -87,7 +87,7 @@
     3.4              })
     3.5        }
     3.6        register(doc)
     3.7 -      prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
     3.8 +      prover.edit_document(change.parent.get.id, doc.id, id_changes)
     3.9      }
    3.10  
    3.11