diff -r c8123e77acc5 -r e1fb3bbc22ab src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 31 16:07:25 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 31 17:35:41 2010 +0200
@@ -180,7 +180,7 @@
   {
     class Fail(state: State) extends Exception
 
-    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
+    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
 
     class Assignment(former_assignment: Map[Command, Exec_ID])
     {
@@ -243,7 +243,7 @@
           }
       }
 
-    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
+    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
     {
       val version = the_version(id)
       val occs = Set(version)  // FIXME unused (!?)
@@ -257,7 +257,7 @@
           (st.command, exec_id)
         }
       the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
-      copy(execs = new_execs)
+      (assigned_execs.map(_._1), copy(execs = new_execs))
     }
 
     def is_assigned(version: Version): Boolean =