src/Pure/PIDE/document.scala
changeset 44479 9a04e7502e22
parent 44477 086bb1083552
child 44484 470f2ee5950e
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 19:12:58 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 26 15:09:54 2011 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  
     1.5    object Change
     1.6    {
     1.7 -    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
     1.8 +    val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
     1.9    }
    1.10  
    1.11    sealed case class Change(
    1.12 @@ -173,7 +173,7 @@
    1.13  
    1.14    object History
    1.15    {
    1.16 -    val init = new History(List(Change.init))
    1.17 +    val init: History = new History(List(Change.init))
    1.18    }
    1.19  
    1.20    // FIXME pruning, purging of state
    1.21 @@ -205,7 +205,7 @@
    1.22    }
    1.23  
    1.24    type Assign =
    1.25 -   (List[(Document.Command_ID, Document.Exec_ID)],  // exec state assignment
    1.26 +   (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
    1.27      List[(String, Option[Document.Command_ID])])  // last exec
    1.28  
    1.29    val no_assign: Assign = (Nil, Nil)
    1.30 @@ -214,8 +214,13 @@
    1.31    {
    1.32      class Fail(state: State) extends Exception
    1.33  
    1.34 -    val init =
    1.35 -      State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2
    1.36 +    val init: State =
    1.37 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
    1.38 +
    1.39 +    object Assignment
    1.40 +    {
    1.41 +      val init: Assignment = Assignment(Map.empty, Map.empty, false)
    1.42 +    }
    1.43  
    1.44      case class Assignment(
    1.45        val command_execs: Map[Command_ID, Exec_ID],
    1.46 @@ -223,12 +228,18 @@
    1.47        val is_finished: Boolean)
    1.48      {
    1.49        def check_finished: Assignment = { require(is_finished); this }
    1.50 -      def assign(add_command_execs: List[(Command_ID, Exec_ID)],
    1.51 +      def unfinished: Assignment = copy(is_finished = false)
    1.52 +
    1.53 +      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
    1.54          add_last_execs: List[(String, Option[Command_ID])]): Assignment =
    1.55        {
    1.56          require(!is_finished)
    1.57 -        // FIXME maintain last_commands
    1.58 -        Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true)
    1.59 +        val command_execs1 =
    1.60 +          (command_execs /: add_command_execs) {
    1.61 +            case (res, (command_id, None)) => res - command_id
    1.62 +            case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
    1.63 +          }
    1.64 +        Assignment(command_execs1, last_execs ++ add_last_execs, true)
    1.65        }
    1.66      }
    1.67    }
    1.68 @@ -243,14 +254,12 @@
    1.69    {
    1.70      private def fail[A]: A = throw new State.Fail(this)
    1.71  
    1.72 -    def define_version(version: Version,
    1.73 -        command_execs: Map[Command_ID, Exec_ID],
    1.74 -        last_execs: Map[String, Option[Command_ID]]): State =
    1.75 +    def define_version(version: Version, assignment: State.Assignment): State =
    1.76      {
    1.77        val id = version.id
    1.78        if (versions.isDefinedAt(id) || disposed(id)) fail
    1.79        copy(versions = versions + (id -> version),
    1.80 -        assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false)))
    1.81 +        assignments = assignments + (id -> assignment.unfinished))
    1.82      }
    1.83  
    1.84      def define_command(command: Command): State =
    1.85 @@ -263,7 +272,7 @@
    1.86      def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
    1.87  
    1.88      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    1.89 -    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    1.90 +    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
    1.91      def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
    1.92      def the_assignment(version: Version): State.Assignment =
    1.93        assignments.getOrElse(version.id, fail)
    1.94 @@ -287,16 +296,16 @@
    1.95        val version = the_version(id)
    1.96        val (command_execs, last_execs) = arg
    1.97  
    1.98 -      val new_execs =
    1.99 -        (execs /: command_execs) {
   1.100 -          case (execs1, (cmd_id, exec_id)) =>
   1.101 -          if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail
   1.102 -          execs1 + (exec_id -> the_command(cmd_id))
   1.103 +      val (commands, new_execs) =
   1.104 +        ((Nil: List[Command], execs) /: command_execs) {
   1.105 +          case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
   1.106 +            val st = the_command(cmd_id)
   1.107 +            (st.command :: commands1, execs1 + (exec_id -> st))
   1.108 +          case (res, (_, None)) => res
   1.109          }
   1.110        val new_assignment = the_assignment(version).assign(command_execs, last_execs)
   1.111        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
   1.112  
   1.113 -      val commands = command_execs.map(p => the_command(p._1).command)
   1.114        (commands, new_state)
   1.115      }
   1.116