Document state assignment indicates command change;

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

--- a/src/Pure/System/session.scala	Tue Aug 31 16:07:25 2010 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 31 17:35:41 2010 +0200
@@ -190,7 +190,8 @@
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
                 try {
-                  global_state.change(_.assign(id, edits))
+                  val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
+                  for (cmd <- cmds) command_change_buffer ! cmd
                   assignments.event(Session.Assignment)
                 }
                 catch { case _: Document.State.Fail => bad_result(result) }