simplified/clarified Change: transition prev --edits--> result, based on futures;
Session.history: plain List instead of somewhat indirect Change.ancestors;
tuned;

--- a/src/Pure/PIDE/document.scala	Thu Aug 12 16:23:04 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 12 17:37:58 2010 +0200
@@ -107,27 +107,17 @@
 
   object Change
   {
-    val init = new Change(None, Nil, Future.value(Nil, Document.init))
+    val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
   }
 
   class Change(
-    val parent: Option[Change],
+    val prev: Future[Document],
     val edits: List[Node_Text_Edit],
     val result: Future[(List[Edit[Command]], Document)])
   {
-    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 join_document: Document = result.join._2
-    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+    val document: Future[Document] = result.map(_._2)
+    def is_finished: Boolean = prev.is_finished && document.is_finished
+    def is_assigned: Boolean = is_finished && document.join.assignment.is_finished
   }
 
 

--- a/src/Pure/System/session.scala	Thu Aug 12 16:23:04 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 12 17:37:58 2010 +0200
@@ -99,9 +99,11 @@
     def handle_change(change: Document.Change)
     //{{{
     {
-      require(change.parent.isDefined)
+      require(change.is_finished)
 
+      val old_id = change.prev.join.id
       val (node_edits, doc) = change.result.join
+
       val id_edits =
         node_edits map {
           case (name, None) => (name, None)
@@ -125,7 +127,7 @@
             (name -> Some(chs))
         }
       register_document(doc)
-      prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits)
+      prover.edit_document(old_id, doc.id, id_edits)
     }
     //}}}
 
@@ -319,23 +321,25 @@
 
   private val editor_history = new Actor
   {
-    @volatile private var history = Document.Change.init
+    @volatile private var history = List(Document.Change.init)
 
     def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
     {
-      val latest = history
-      val stable = latest.ancestors.find(_.is_assigned)
-      require(stable.isDefined)
+      val history_snapshot = history
+
+      require(history_snapshot.exists(_.is_assigned))
+      val latest = history_snapshot.head
+      val stable = history_snapshot.find(_.is_assigned).get
 
       val edits =
-        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+        (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
       lazy val reverse_edits = edits.reverse
 
       new Document.Snapshot {
-        val document = stable.get.join_document
+        val document = stable.document.join
         val node = document.nodes(name)
-        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable)
         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
         def state(command: Command): Command.State = document.current_state(command)
@@ -347,16 +351,19 @@
       loop {
         react {
           case Edit_Document(edits) =>
-            val old_change = history
+            val history_snapshot = history
+            require(!history_snapshot.isEmpty)
+
+            val prev = history_snapshot.head.document
             val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
               isabelle.Future.fork {
-                val old_doc = old_change.join_document
+                val old_doc = prev.join
                 old_doc.await_assignment
                 Document.text_edits(Session.this, old_doc, edits)
               }
-            val new_change = new Document.Change(Some(old_change), edits, result)
-            history = new_change
-            new_change.result.map(_ => session_actor ! new_change)
+            val new_change = new Document.Change(prev, edits, result)
+            history ::= new_change
+            new_change.document.map(_ => session_actor ! new_change)
             reply(())
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)