maintain last_execs assignment on Scala side;
prefer tables over IDs instead of objects;

--- a/src/Pure/PIDE/document.scala	Thu Aug 25 16:44:06 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 25 17:38:12 2011 +0200
@@ -214,19 +214,21 @@
   {
     class Fail(state: State) extends Exception
 
-    val init = State().define_version(Version.init, Map()).assign(Version.init.id, no_assign)._2
+    val init =
+      State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2
 
     case class Assignment(
-      val assignment: Map[Command, Exec_ID],
-      val is_finished: Boolean = false)
+      val command_execs: Map[Command_ID, Exec_ID],
+      val last_execs: Map[String, Option[Command_ID]],
+      val is_finished: Boolean)
     {
-      def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
-      def assign(command_execs: List[(Command, Exec_ID)],
-        last_commands: List[(String, Option[Command])]): Assignment =
+      def check_finished: Assignment = { require(is_finished); this }
+      def assign(add_command_execs: List[(Command_ID, Exec_ID)],
+        add_last_execs: List[(String, Option[Command_ID])]): Assignment =
       {
         require(!is_finished)
         // FIXME maintain last_commands
-        Assignment(assignment ++ command_execs, true)
+        Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true)
       }
     }
   }
@@ -241,12 +243,14 @@
   {
     private def fail[A]: A = throw new State.Fail(this)
 
-    def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
+    def define_version(version: Version,
+        command_execs: Map[Command_ID, Exec_ID],
+        last_execs: Map[String, Option[Command_ID]]): State =
     {
       val id = version.id
       if (versions.isDefinedAt(id) || disposed(id)) fail
       copy(versions = versions + (id -> version),
-        assignments = assignments + (id -> State.Assignment(former_assignment)))
+        assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false)))
     }
 
     def define_command(command: Command): State =
@@ -281,25 +285,19 @@
     def assign(id: Version_ID, arg: Assign): (List[Command], State) =
     {
       val version = the_version(id)
-      val (edits, last_ids) = arg
+      val (command_execs, last_execs) = arg
 
-      var new_execs = execs
-      val assigned_execs =
-        for ((cmd_id, exec_id) <- edits) yield {
-          val st = the_command(cmd_id)
-          if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
-          new_execs += (exec_id -> st)
-          (st.command, exec_id)
+      val new_execs =
+        (execs /: command_execs) {
+          case (execs1, (cmd_id, exec_id)) =>
+          if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail
+          execs1 + (exec_id -> the_command(cmd_id))
         }
-
-      val last_commands =
-        last_ids map {
-          case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command))
-          case (name, None) => (name, None) }
-      val new_assignment = the_assignment(version).assign(assigned_execs, last_commands)
+      val new_assignment = the_assignment(version).assign(command_execs, last_execs)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
 
-      (assigned_execs.map(_._1), new_state)
+      val commands = command_execs.map(p => the_command(p._1).command)
+      (commands, new_state)
     }
 
     def is_assigned(version: Version): Boolean =
@@ -346,7 +344,10 @@
         def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
 
         def state(command: Command): Command.State =
-          try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
+          try {
+            the_exec(the_assignment(version).check_finished.command_execs
+              .getOrElse(command.id, fail))
+          }
           catch { case _: State.Fail => command.empty_state }
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))

--- a/src/Pure/System/session.scala	Thu Aug 25 16:44:06 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 25 17:38:12 2011 +0200
@@ -215,8 +215,8 @@
         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))
+      val assignment = global_state().the_assignment(previous).check_finished
+      global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs))
       global_state.change_yield(_.assign(version.id, Document.no_assign))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
@@ -268,12 +268,14 @@
       val name = change.name
       val doc_edits = change.doc_edits
 
-      var former_assignment = global_state().the_assignment(previous).get_finished
+      val previous_assignment = global_state().the_assignment(previous).check_finished
+
+      var command_execs = previous_assignment.command_execs
       for {
         (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
         (prev, None) <- cmd_edits
         removed <- previous.nodes(name).commands.get_after(prev)
-      } former_assignment -= removed
+      } command_execs -= removed.id
 
       def id_command(command: Command)
       {
@@ -287,7 +289,7 @@
           edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
       }
 
-      global_state.change(_.define_version(version, former_assignment))
+      global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs))
       prover.get.edit_version(previous.id, version.id, doc_edits)
     }
     //}}}