1.1 --- a/src/Pure/System/session.scala	Thu Aug 25 16:44:06 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Aug 25 17:38:12 2011 +0200
     1.3 @@ -215,8 +215,8 @@
     1.4          global_state.change_yield(
     1.5            _.continue_history(Future.value(previous), text_edits, Future.value(version)))
     1.6  
     1.7 -      val assignment = global_state().the_assignment(previous).get_finished
     1.8 -      global_state.change(_.define_version(version, assignment))
     1.9 +      val assignment = global_state().the_assignment(previous).check_finished
    1.10 +      global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs))
    1.11        global_state.change_yield(_.assign(version.id, Document.no_assign))
    1.12  
    1.13        prover.get.update_perspective(previous.id, version.id, name, perspective)
    1.14 @@ -268,12 +268,14 @@
    1.15        val name = change.name
    1.16        val doc_edits = change.doc_edits
    1.17  
    1.18 -      var former_assignment = global_state().the_assignment(previous).get_finished
    1.19 +      val previous_assignment = global_state().the_assignment(previous).check_finished
    1.20 +
    1.21 +      var command_execs = previous_assignment.command_execs
    1.22        for {
    1.23          (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
    1.24          (prev, None) <- cmd_edits
    1.25          removed <- previous.nodes(name).commands.get_after(prev)
    1.26 -      } former_assignment -= removed
    1.27 +      } command_execs -= removed.id
    1.28  
    1.29        def id_command(command: Command)
    1.30        {
    1.31 @@ -287,7 +289,7 @@
    1.32            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
    1.33        }
    1.34  
    1.35 -      global_state.change(_.define_version(version, former_assignment))
    1.36 +      global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs))
    1.37        prover.get.edit_version(previous.id, version.id, doc_edits)
    1.38      }
    1.39      //}}}