1.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 30 20:12:43 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 31 12:49:40 2010 +0200
     1.3 @@ -44,7 +44,6 @@
     1.4    {
     1.5      val empty: Node = new Node(Linear_Set())
     1.6  
     1.7 -    // FIXME not scalable
     1.8      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
     1.9        : Iterator[(Command, Text.Offset)] =
    1.10      {
    1.11 @@ -57,16 +56,36 @@
    1.12      }
    1.13    }
    1.14  
    1.15 +  private val block_size = 4096
    1.16 +
    1.17    class Node(val commands: Linear_Set[Command])
    1.18    {
    1.19 -    def command_starts: Iterator[(Command, Text.Offset)] =
    1.20 -      Node.command_starts(commands.iterator)
    1.21 +    private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    1.22 +    {
    1.23 +      val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
    1.24 +      var next_block = 0
    1.25 +      var last_stop = 0
    1.26 +      for ((command, start) <- Node.command_starts(commands.iterator)) {
    1.27 +        last_stop = start + command.length
    1.28 +        if (last_stop + 1 > next_block) {
    1.29 +          blocks += (command -> start)
    1.30 +          next_block += block_size
    1.31 +        }
    1.32 +      }
    1.33 +      (blocks.toArray, Text.Range(0, last_stop))
    1.34 +    }
    1.35  
    1.36 -    def command_start(cmd: Command): Option[Text.Offset] =
    1.37 -      command_starts.find(_._1 == cmd).map(_._2)
    1.38 +    def full_range: Text.Range = full_index._2
    1.39  
    1.40      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.41 -      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    1.42 +    {
    1.43 +      if (!commands.isEmpty && full_range.contains(i)) {
    1.44 +        val (cmd0, start0) = full_index._1(i / block_size)
    1.45 +        Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
    1.46 +          case (cmd, start) => start + cmd.length <= i }
    1.47 +      }
    1.48 +      else Iterator.empty
    1.49 +    }
    1.50  
    1.51      def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
    1.52        command_range(range.start) takeWhile { case (_, start) => start < range.stop }
    1.53 @@ -83,6 +102,12 @@
    1.54            commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    1.55          case None => None
    1.56        }
    1.57 +
    1.58 +    def command_start(cmd: Command): Option[Text.Offset] =
    1.59 +      command_starts.find(_._1 == cmd).map(_._2)
    1.60 +
    1.61 +    def command_starts: Iterator[(Command, Text.Offset)] =
    1.62 +      Node.command_starts(commands.iterator)
    1.63    }
    1.64  
    1.65