src/Pure/System/session.scala

--- 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)