1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 31 16:07:25 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 31 17:35:41 2010 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4    {
     1.5      class Fail(state: State) extends Exception
     1.6  
     1.7 -    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
     1.8 +    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
     1.9  
    1.10      class Assignment(former_assignment: Map[Command, Exec_ID])
    1.11      {
    1.12 @@ -243,7 +243,7 @@
    1.13            }
    1.14        }
    1.15  
    1.16 -    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
    1.17 +    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
    1.18      {
    1.19        val version = the_version(id)
    1.20        val occs = Set(version)  // FIXME unused (!?)
    1.21 @@ -257,7 +257,7 @@
    1.22            (st.command, exec_id)
    1.23          }
    1.24        the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
    1.25 -      copy(execs = new_execs)
    1.26 +      (assigned_execs.map(_._1), copy(execs = new_execs))
    1.27      }
    1.28  
    1.29      def is_assigned(version: Version): Boolean =

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