src/Pure/PIDE/document.scala
changeset 46208 4cab63a6dc16
parent 46198 cd040c5772de
child 46677 388ba4daae05
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Jan 14 14:34:42 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Jan 14 15:20:29 2012 +0100
     1.3 @@ -234,7 +234,6 @@
     1.4      val version: Version
     1.5      val node: Node
     1.6      val is_outdated: Boolean
     1.7 -    def command_state(command: Command): Command.State
     1.8      def convert(i: Text.Offset): Text.Offset
     1.9      def convert(range: Text.Range): Text.Range
    1.10      def revert(i: Text.Offset): Text.Offset
    1.11 @@ -465,7 +464,6 @@
    1.12          val version = stable.version.get_finished
    1.13          val node = version.nodes(name)
    1.14          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.15 -        def command_state(command: Command): Command.State = state.command_state(version, command)
    1.16  
    1.17          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.18          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.19 @@ -478,7 +476,7 @@
    1.20            val former_range = revert(range)
    1.21            for {
    1.22              (command, command_start) <- node.command_range(former_range).toStream
    1.23 -            Text.Info(r0, a) <- command_state(command).markup.
    1.24 +            Text.Info(r0, a) <- state.command_state(version, command).markup.
    1.25                cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.26                  {
    1.27                    case (a, Text.Info(r0, b))