src/Pure/PIDE/document.scala
changeset 56475 710dee42b3d0
parent 56473 5b5c750e9763
child 56489 884e8f37492c
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 21:48:09 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 22:01:08 2014 +0200
     1.3 @@ -494,7 +494,7 @@
     1.4      /*command-exec assignment for each version*/
     1.5      val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
     1.6      /*commands with markup produced by other commands (imm_succs)*/
     1.7 -    val augmented_commands: Graph[Document_ID.Command, Unit] = Graph.long,
     1.8 +    val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
     1.9      /*explicit (linear) history*/
    1.10      val history: History = History.init)
    1.11    {
    1.12 @@ -540,8 +540,8 @@
    1.13        (execs.get(id) orElse commands.get(id)).map(st =>
    1.14          ((Text.Chunk.Id(st.command.id), st.command.chunk)))
    1.15  
    1.16 -    private def augmented(st: Command.State): Graph[Document_ID.Command, Unit] =
    1.17 -      (augmented_commands /: st.markups.other_id_iterator)({ case (graph, id) =>
    1.18 +    private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
    1.19 +      (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
    1.20          graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
    1.21  
    1.22      def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
    1.23 @@ -550,13 +550,13 @@
    1.24          case Some(st) =>
    1.25            val new_st = st.accumulate(self_id(st), other_id _, message)
    1.26            val execs1 = execs + (id -> new_st)
    1.27 -          (new_st, copy(execs = execs1, augmented_commands = augmented(new_st)))
    1.28 +          (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
    1.29          case None =>
    1.30            commands.get(id) match {
    1.31              case Some(st) =>
    1.32                val new_st = st.accumulate(self_id(st), other_id _, message)
    1.33                val commands1 = commands + (id -> new_st)
    1.34 -              (new_st, copy(commands = commands1, augmented_commands = augmented(new_st)))
    1.35 +              (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
    1.36              case None => fail
    1.37            }
    1.38        }
    1.39 @@ -654,7 +654,7 @@
    1.40          blobs = blobs1,
    1.41          commands = commands1,
    1.42          execs = execs1,
    1.43 -        augmented_commands = augmented_commands.restrict(commands1.isDefinedAt(_)),
    1.44 +        commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
    1.45          assignments = assignments1)
    1.46      }
    1.47  
    1.48 @@ -680,15 +680,15 @@
    1.49      {
    1.50        val self = command_states_self(version, command)
    1.51        val others =
    1.52 -        if (augmented_commands.defined(command.id)) {
    1.53 +        if (commands_redirection.defined(command.id)) {
    1.54            (for {
    1.55 -            command_id <- augmented_commands.imm_succs(command.id).iterator
    1.56 +            command_id <- commands_redirection.imm_succs(command.id).iterator
    1.57              (id, st) <- command_states_self(version, the_static_state(command_id).command)
    1.58              if !self.exists(_._1 == id)
    1.59            } yield (id, st)).toMap.valuesIterator.toList
    1.60          }
    1.61          else Nil
    1.62 -      self.map(_._2) ::: others.map(_.retarget(command))
    1.63 +      self.map(_._2) ::: others.map(_.redirect(command))
    1.64      }
    1.65  
    1.66      def command_results(version: Version, command: Command): Command.Results =