1.1 --- a/src/Pure/System/session.scala	Thu Aug 25 19:12:58 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Fri Aug 26 15:09:54 2011 +0200
     1.3 @@ -216,7 +216,7 @@
     1.4            _.continue_history(Future.value(previous), text_edits, Future.value(version)))
     1.5  
     1.6        val assignment = global_state().the_assignment(previous).check_finished
     1.7 -      global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs))
     1.8 +      global_state.change(_.define_version(version, assignment))
     1.9        global_state.change_yield(_.assign(version.id, Document.no_assign))
    1.10  
    1.11        prover.get.update_perspective(previous.id, version.id, name, perspective)
    1.12 @@ -268,15 +268,6 @@
    1.13        val name = change.name
    1.14        val doc_edits = change.doc_edits
    1.15  
    1.16 -      val previous_assignment = global_state().the_assignment(previous).check_finished
    1.17 -
    1.18 -      var command_execs = previous_assignment.command_execs
    1.19 -      for {
    1.20 -        (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
    1.21 -        (prev, None) <- cmd_edits
    1.22 -        removed <- previous.nodes(name).commands.get_after(prev)
    1.23 -      } command_execs -= removed.id
    1.24 -
    1.25        def id_command(command: Command)
    1.26        {
    1.27          if (global_state().lookup_command(command.id).isEmpty) {
    1.28 @@ -289,7 +280,8 @@
    1.29            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
    1.30        }
    1.31  
    1.32 -      global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs))
    1.33 +      val assignment = global_state().the_assignment(previous).check_finished
    1.34 +      global_state.change(_.define_version(version, assignment))
    1.35        prover.get.edit_version(previous.id, version.id, doc_edits)
    1.36      }
    1.37      //}}}
    1.38 @@ -388,9 +380,10 @@
    1.39            reply(())
    1.40  
    1.41          case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
    1.42 -          if (text_edits.isEmpty && global_state().tip_stable)
    1.43 -            update_perspective(name, perspective)
    1.44 -          else
    1.45 +// FIXME
    1.46 +//          if (text_edits.isEmpty && global_state().tip_stable)
    1.47 +//            update_perspective(name, perspective)
    1.48 +//          else
    1.49              handle_edits(name, master_dir, header,
    1.50                List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
    1.51            reply(())