src/Pure/PIDE/document.scala
changeset 47388 fe4b245af74c
parent 46997 395b7277ed76
child 47395 e6261a493f04
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Apr 06 14:40:00 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Apr 06 23:34:38 2012 +0200
     1.3 @@ -296,9 +296,7 @@
     1.4        result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
     1.5    }
     1.6  
     1.7 -  type Assign =
     1.8 -   (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
     1.9 -    List[(String, Option[Document.Command_ID])])  // last exec
    1.10 +  type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
    1.11  
    1.12    object State
    1.13    {
    1.14 @@ -311,14 +309,12 @@
    1.15  
    1.16      final class Assignment private(
    1.17        val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
    1.18 -      val last_execs: Map[String, Option[Command_ID]] = Map.empty,
    1.19        val is_finished: Boolean = false)
    1.20      {
    1.21        def check_finished: Assignment = { require(is_finished); this }
    1.22 -      def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
    1.23 +      def unfinished: Assignment = new Assignment(command_execs, false)
    1.24  
    1.25 -      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
    1.26 -        add_last_execs: List[(String, Option[Command_ID])]): Assignment =
    1.27 +      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
    1.28        {
    1.29          require(!is_finished)
    1.30          val command_execs1 =
    1.31 @@ -326,7 +322,7 @@
    1.32              case (res, (command_id, None)) => res - command_id
    1.33              case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
    1.34            }
    1.35 -        new Assignment(command_execs1, last_execs ++ add_last_execs, true)
    1.36 +        new Assignment(command_execs1, true)
    1.37        }
    1.38      }
    1.39  
    1.40 @@ -387,10 +383,9 @@
    1.41            }
    1.42        }
    1.43  
    1.44 -    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
    1.45 +    def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
    1.46      {
    1.47        val version = the_version(id)
    1.48 -      val (command_execs, last_execs) = arg
    1.49  
    1.50        val (changed_commands, new_execs) =
    1.51          ((Nil: List[Command], execs) /: command_execs) {
    1.52 @@ -404,7 +399,7 @@
    1.53                }
    1.54              (commands2, execs2)
    1.55          }
    1.56 -      val new_assignment = the_assignment(version).assign(command_execs, last_execs)
    1.57 +      val new_assignment = the_assignment(version).assign(command_execs)
    1.58        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.59  
    1.60        (changed_commands, new_state)
    1.61 @@ -424,21 +419,6 @@
    1.62      def tip_stable: Boolean = is_stable(history.tip)
    1.63      def tip_version: Version = history.tip.version.get_finished
    1.64  
    1.65 -    def last_exec_offset(name: Node.Name): Text.Offset =
    1.66 -    {
    1.67 -      val version = tip_version
    1.68 -      the_assignment(version).last_execs.get(name.node) match {
    1.69 -        case Some(Some(id)) =>
    1.70 -          val node = version.nodes(name)
    1.71 -          val cmd = the_command(id).command
    1.72 -          node.command_start(cmd) match {
    1.73 -            case None => 0
    1.74 -            case Some(start) => start + cmd.length
    1.75 -          }
    1.76 -        case _ => 0
    1.77 -      }
    1.78 -    }
    1.79 -
    1.80      def continue_history(
    1.81          previous: Future[Version],
    1.82          edits: List[Edit_Text],