# HG changeset patch
# User wenzelm
# Date 1283268941 -7200
# Node ID e1fb3bbc22aba6e7a892224661aa4c13aa52c740
# Parent  c8123e77acc5595865a74430baf77aeef4ae69e7
Document state assignment indicates command change;

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 =
diff -r c8123e77acc5 -r e1fb3bbc22ab src/Pure/System/session.scala
--- 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) }