src/Pure/PIDE/document.scala
changeset 44476 e8a87398f35d
parent 44475 709e1d671483
child 44477 086bb1083552
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 13:24:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 25 16:44:06 2011 +0200
     1.3 @@ -204,20 +204,28 @@
     1.4        : Stream[Text.Info[Option[A]]]
     1.5    }
     1.6  
     1.7 +  type Assign =
     1.8 +   (List[(Document.Command_ID, Document.Exec_ID)],  // exec state assignment
     1.9 +    List[(String, Option[Document.Command_ID])])  // last exec
    1.10 +
    1.11 +  val no_assign: Assign = (Nil, Nil)
    1.12 +
    1.13    object State
    1.14    {
    1.15      class Fail(state: State) extends Exception
    1.16  
    1.17 -    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
    1.18 +    val init = State().define_version(Version.init, Map()).assign(Version.init.id, no_assign)._2
    1.19  
    1.20      case class Assignment(
    1.21        val assignment: Map[Command, Exec_ID],
    1.22        val is_finished: Boolean = false)
    1.23      {
    1.24        def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
    1.25 -      def assign(command_execs: List[(Command, Exec_ID)]): Assignment =
    1.26 +      def assign(command_execs: List[(Command, Exec_ID)],
    1.27 +        last_commands: List[(String, Option[Command])]): Assignment =
    1.28        {
    1.29          require(!is_finished)
    1.30 +        // FIXME maintain last_commands
    1.31          Assignment(assignment ++ command_execs, true)
    1.32        }
    1.33      }
    1.34 @@ -270,9 +278,10 @@
    1.35            }
    1.36        }
    1.37  
    1.38 -    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
    1.39 +    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
    1.40      {
    1.41        val version = the_version(id)
    1.42 +      val (edits, last_ids) = arg
    1.43  
    1.44        var new_execs = execs
    1.45        val assigned_execs =
    1.46 @@ -282,8 +291,14 @@
    1.47            new_execs += (exec_id -> st)
    1.48            (st.command, exec_id)
    1.49          }
    1.50 -      val new_assignment = the_assignment(version).assign(assigned_execs)
    1.51 +
    1.52 +      val last_commands =
    1.53 +        last_ids map {
    1.54 +          case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command))
    1.55 +          case (name, None) => (name, None) }
    1.56 +      val new_assignment = the_assignment(version).assign(assigned_execs, last_commands)
    1.57        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.58 +
    1.59        (assigned_execs.map(_._1), new_state)
    1.60      }
    1.61