src/Pure/System/session.scala

         global_state.change_yield(
           _.continue_history(Future.value(previous), text_edits, Future.value(version)))
 
       val assignment = global_state().the_assignment(previous).get_finished
       global_state.change(_.define_version(version, assignment))
-      global_state.change_yield(_.assign(version.id, Nil))
+      global_state.change_yield(_.assign(version.id, Document.no_assign))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
     }
 
 

     //}}}
 
 
     /* exec state assignment */
 
-    def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+    def handle_assign(id: Document.Version_ID, assign: Document.Assign)
     //{{{
     {
-      val cmds = global_state.change_yield(_.assign(id, edits))
+      val cmds = global_state.change_yield(_.assign(id, assign))
       for (cmd <- cmds) command_change_buffer ! cmd
       assignments.event(Session.Assignment)
     }
     //}}}
 

             else if (result.is_exit) phase = Session.Inactive
           }
           else if (result.is_stdout) { }
           else if (result.is_status) {
             result.body match {
-              case List(Isar_Document.Assign(id, edits)) =>
-                try { handle_assign(id, edits) }
+              case List(Isar_Document.Assign(id, assign)) =>
+                try { handle_assign(id, assign) }
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
               case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
               case _ => bad_result(result)