1.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -45,7 +45,8 @@
     1.4      val empty: Node = new Node(Linear_Set())
     1.5  
     1.6      // FIXME not scalable
     1.7 -    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
     1.8 +    def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
     1.9 +      : Iterator[(Command, Text.Offset)] =
    1.10      {
    1.11        var i = offset
    1.12        for (command <- commands) yield {
    1.13 @@ -58,25 +59,25 @@
    1.14  
    1.15    class Node(val commands: Linear_Set[Command])
    1.16    {
    1.17 -    def command_starts: Iterator[(Command, Int)] =
    1.18 +    def command_starts: Iterator[(Command, Text.Offset)] =
    1.19        Node.command_starts(commands.iterator)
    1.20  
    1.21 -    def command_start(cmd: Command): Option[Int] =
    1.22 +    def command_start(cmd: Command): Option[Text.Offset] =
    1.23        command_starts.find(_._1 == cmd).map(_._2)
    1.24  
    1.25 -    def command_range(i: Int): Iterator[(Command, Int)] =
    1.26 +    def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
    1.27        command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    1.28  
    1.29 -    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
    1.30 +    def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
    1.31        command_range(i) takeWhile { case (_, start) => start < j }
    1.32  
    1.33 -    def command_at(i: Int): Option[(Command, Int)] =
    1.34 +    def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
    1.35      {
    1.36        val range = command_range(i)
    1.37        if (range.hasNext) Some(range.next) else None
    1.38      }
    1.39  
    1.40 -    def proper_command_at(i: Int): Option[Command] =
    1.41 +    def proper_command_at(i: Text.Offset): Option[Command] =
    1.42        command_at(i) match {
    1.43          case Some((command, _)) =>
    1.44            commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    1.45 @@ -122,8 +123,8 @@
    1.46      val version: Version
    1.47      val node: Node
    1.48      val is_outdated: Boolean
    1.49 -    def convert(offset: Int): Int
    1.50 -    def revert(offset: Int): Int
    1.51 +    def convert(i: Text.Offset): Text.Offset
    1.52 +    def revert(i: Text.Offset): Text.Offset
    1.53      def lookup_command(id: Command_ID): Option[Command]
    1.54      def state(command: Command): Command.State
    1.55    }
    1.56 @@ -159,8 +160,10 @@
    1.57          val version = stable.current.join
    1.58          val node = version.nodes(name)
    1.59          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.60 -        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    1.61 -        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.62 +
    1.63 +        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.64 +        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.65 +
    1.66          def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
    1.67          def state(command: Command): Command.State =
    1.68            try { state_snapshot.command_state(version, command) }