recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
Change.ancestors: frugal iterator;

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 03 20:50:07 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 03 23:03:04 2010 +0100
@@ -58,8 +58,10 @@
 {
   /* history */
 
+  private val document_0 = session.begin_document(buffer.getName)
+
   @volatile private var history =  // owned by Swing thread
-    new Change(None, Nil, Future.value(session.begin_document(buffer.getName), Nil))
+    new Change(None, Nil, document_0.id, Future.value(document_0, Nil))
 
   def current_change(): Change = history
 
@@ -77,8 +79,8 @@
   private def changes_from(doc: Document): List[Edit] =
   {
     Swing_Thread.assert()
-    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
-      edits_buffer.toList
+    (edits_buffer.toList /:
+      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
   }
 
   def from_current(doc: Document, offset: Int): Int =
@@ -103,10 +105,11 @@
     if (!edits_buffer.isEmpty) {
       val edits = edits_buffer.toList
       val change1 = current_change()
+      val result_id = session.create_id()
       val result: Future[Document.Result] = Future.fork {
-        Document.text_edits(session, change1.document, session.create_id(), edits)
+        Document.text_edits(session, change1.document, result_id, edits)
       }
-      val change2 = new Change(Some(change1), edits, result)
+      val change2 = new Change(Some(change1), edits, result_id, result)
       history = change2
       result.map(_ => session.input(change2))
       edits_buffer.clear

--- a/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 03 20:50:07 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 03 23:03:04 2010 +0100
@@ -42,13 +42,19 @@
 class Change(
   val parent: Option[Change],
   val edits: List[Edit],
+  val id: Isar_Document.Document_ID,
   val result: Future[Document.Result])
 {
-  // FIXME iterator
-  def ancestors(done: Change => Boolean): List[Change] =
-    if (done(this)) Nil
-    else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
-  def ancestors: List[Change] = ancestors(_ => false)
+  def ancestors: Iterator[Change] = new Iterator[Change]
+  {
+    private var state: Option[Change] = Some(Change.this)
+    def hasNext = state.isDefined
+    def next =
+      state match {
+        case Some(change) => state = change.parent; change
+        case None => throw new NoSuchElementException("next on empty iterator")
+      }
+  }
 
   def document: Document = result.join._1
   def document_edits: List[Document.Structure_Edit] = result.join._2

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 03 20:50:07 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 03 23:03:04 2010 +0100
@@ -87,7 +87,7 @@
             })
       }
       register(doc)
-      prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
+      prover.edit_document(change.parent.get.id, doc.id, id_changes)
     }