maintain last_execs assignment on Scala side;
authorwenzelm
Thu Aug 25 17:38:12 2011 +0200 (2011-08-25 ago)
changeset 44477086bb1083552
parent 44476 e8a87398f35d
child 44478 4fdb1009a370
maintain last_execs assignment on Scala side;
prefer tables over IDs instead of objects;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 16:44:06 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 25 17:38:12 2011 +0200
     1.3 @@ -214,19 +214,21 @@
     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, no_assign)._2
     1.8 +    val init =
     1.9 +      State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2
    1.10  
    1.11      case class Assignment(
    1.12 -      val assignment: Map[Command, Exec_ID],
    1.13 -      val is_finished: Boolean = false)
    1.14 +      val command_execs: Map[Command_ID, Exec_ID],
    1.15 +      val last_execs: Map[String, Option[Command_ID]],
    1.16 +      val is_finished: Boolean)
    1.17      {
    1.18 -      def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
    1.19 -      def assign(command_execs: List[(Command, Exec_ID)],
    1.20 -        last_commands: List[(String, Option[Command])]): Assignment =
    1.21 +      def check_finished: Assignment = { require(is_finished); this }
    1.22 +      def assign(add_command_execs: List[(Command_ID, Exec_ID)],
    1.23 +        add_last_execs: List[(String, Option[Command_ID])]): Assignment =
    1.24        {
    1.25          require(!is_finished)
    1.26          // FIXME maintain last_commands
    1.27 -        Assignment(assignment ++ command_execs, true)
    1.28 +        Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true)
    1.29        }
    1.30      }
    1.31    }
    1.32 @@ -241,12 +243,14 @@
    1.33    {
    1.34      private def fail[A]: A = throw new State.Fail(this)
    1.35  
    1.36 -    def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
    1.37 +    def define_version(version: Version,
    1.38 +        command_execs: Map[Command_ID, Exec_ID],
    1.39 +        last_execs: Map[String, Option[Command_ID]]): State =
    1.40      {
    1.41        val id = version.id
    1.42        if (versions.isDefinedAt(id) || disposed(id)) fail
    1.43        copy(versions = versions + (id -> version),
    1.44 -        assignments = assignments + (id -> State.Assignment(former_assignment)))
    1.45 +        assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false)))
    1.46      }
    1.47  
    1.48      def define_command(command: Command): State =
    1.49 @@ -281,25 +285,19 @@
    1.50      def assign(id: Version_ID, arg: Assign): (List[Command], State) =
    1.51      {
    1.52        val version = the_version(id)
    1.53 -      val (edits, last_ids) = arg
    1.54 +      val (command_execs, last_execs) = arg
    1.55  
    1.56 -      var new_execs = execs
    1.57 -      val assigned_execs =
    1.58 -        for ((cmd_id, exec_id) <- edits) yield {
    1.59 -          val st = the_command(cmd_id)
    1.60 -          if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
    1.61 -          new_execs += (exec_id -> st)
    1.62 -          (st.command, exec_id)
    1.63 +      val new_execs =
    1.64 +        (execs /: command_execs) {
    1.65 +          case (execs1, (cmd_id, exec_id)) =>
    1.66 +          if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail
    1.67 +          execs1 + (exec_id -> the_command(cmd_id))
    1.68          }
    1.69 -
    1.70 -      val last_commands =
    1.71 -        last_ids map {
    1.72 -          case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command))
    1.73 -          case (name, None) => (name, None) }
    1.74 -      val new_assignment = the_assignment(version).assign(assigned_execs, last_commands)
    1.75 +      val new_assignment = the_assignment(version).assign(command_execs, last_execs)
    1.76        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.77  
    1.78 -      (assigned_execs.map(_._1), new_state)
    1.79 +      val commands = command_execs.map(p => the_command(p._1).command)
    1.80 +      (commands, new_state)
    1.81      }
    1.82  
    1.83      def is_assigned(version: Version): Boolean =
    1.84 @@ -346,7 +344,10 @@
    1.85          def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
    1.86  
    1.87          def state(command: Command): Command.State =
    1.88 -          try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
    1.89 +          try {
    1.90 +            the_exec(the_assignment(version).check_finished.command_execs
    1.91 +              .getOrElse(command.id, fail))
    1.92 +          }
    1.93            catch { case _: State.Fail => command.empty_state }
    1.94  
    1.95          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
     2.1 --- a/src/Pure/System/session.scala	Thu Aug 25 16:44:06 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Aug 25 17:38:12 2011 +0200
     2.3 @@ -215,8 +215,8 @@
     2.4          global_state.change_yield(
     2.5            _.continue_history(Future.value(previous), text_edits, Future.value(version)))
     2.6  
     2.7 -      val assignment = global_state().the_assignment(previous).get_finished
     2.8 -      global_state.change(_.define_version(version, assignment))
     2.9 +      val assignment = global_state().the_assignment(previous).check_finished
    2.10 +      global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs))
    2.11        global_state.change_yield(_.assign(version.id, Document.no_assign))
    2.12  
    2.13        prover.get.update_perspective(previous.id, version.id, name, perspective)
    2.14 @@ -268,12 +268,14 @@
    2.15        val name = change.name
    2.16        val doc_edits = change.doc_edits
    2.17  
    2.18 -      var former_assignment = global_state().the_assignment(previous).get_finished
    2.19 +      val previous_assignment = global_state().the_assignment(previous).check_finished
    2.20 +
    2.21 +      var command_execs = previous_assignment.command_execs
    2.22        for {
    2.23          (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
    2.24          (prev, None) <- cmd_edits
    2.25          removed <- previous.nodes(name).commands.get_after(prev)
    2.26 -      } former_assignment -= removed
    2.27 +      } command_execs -= removed.id
    2.28  
    2.29        def id_command(command: Command)
    2.30        {
    2.31 @@ -287,7 +289,7 @@
    2.32            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
    2.33        }
    2.34  
    2.35 -      global_state.change(_.define_version(version, former_assignment))
    2.36 +      global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs))
    2.37        prover.get.edit_version(previous.id, version.id, doc_edits)
    2.38      }
    2.39      //}}}