src/Pure/PIDE/command.scala
changeset 56475 710dee42b3d0
parent 56473 5b5c750e9763
child 56476 dd596c2b5897
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 21:48:09 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 22:01:08 2014 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4      def add(index: Markup_Index, markup: Text.Markup): Markups =
     1.5        new Markups(rep + (index -> (this(index) + markup)))
     1.6  
     1.7 -    def other_id_iterator: Iterator[Document_ID.Generic] =
     1.8 -      for (Markup_Index(_, Text.Chunk.Id(other_id)) <- rep.keysIterator)
     1.9 -        yield other_id
    1.10 +    def redirection_iterator: Iterator[Document_ID.Generic] =
    1.11 +      for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
    1.12 +        yield id
    1.13  
    1.14 -    def retarget(other_id: Document_ID.Generic): Markups =
    1.15 +    def redirect(other_id: Document_ID.Generic): Markups =
    1.16        new Markups(
    1.17          (for {
    1.18            (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    1.19 @@ -135,8 +135,8 @@
    1.20  
    1.21      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.22  
    1.23 -    def retarget(other_command: Command): State =
    1.24 -      new State(other_command, Nil, Results.empty, markups.retarget(other_command.id))
    1.25 +    def redirect(other_command: Command): State =
    1.26 +      new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
    1.27  
    1.28  
    1.29      def eq_content(other: State): Boolean =