Document.Node: significant speedup of command_range etc. via lazy full_index;

--- a/src/Pure/PIDE/document.scala	Mon Aug 30 20:12:43 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 31 12:49:40 2010 +0200
@@ -44,7 +44,6 @@
   {
     val empty: Node = new Node(Linear_Set())
 
-    // FIXME not scalable
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -57,16 +56,36 @@
     }
   }
 
+  private val block_size = 4096
+
   class Node(val commands: Linear_Set[Command])
   {
-    def command_starts: Iterator[(Command, Text.Offset)] =
-      Node.command_starts(commands.iterator)
+    private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
+    {
+      val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
+      var next_block = 0
+      var last_stop = 0
+      for ((command, start) <- Node.command_starts(commands.iterator)) {
+        last_stop = start + command.length
+        if (last_stop + 1 > next_block) {
+          blocks += (command -> start)
+          next_block += block_size
+        }
+      }
+      (blocks.toArray, Text.Range(0, last_stop))
+    }
 
-    def command_start(cmd: Command): Option[Text.Offset] =
-      command_starts.find(_._1 == cmd).map(_._2)
+    def full_range: Text.Range = full_index._2
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
-      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+    {
+      if (!commands.isEmpty && full_range.contains(i)) {
+        val (cmd0, start0) = full_index._1(i / block_size)
+        Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
+          case (cmd, start) => start + cmd.length <= i }
+      }
+      else Iterator.empty
+    }
 
     def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
       command_range(range.start) takeWhile { case (_, start) => start < range.stop }
@@ -83,6 +102,12 @@
           commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
         case None => None
       }
+
+    def command_start(cmd: Command): Option[Text.Offset] =
+      command_starts.find(_._1 == cmd).map(_._2)
+
+    def command_starts: Iterator[(Command, Text.Offset)] =
+      Node.command_starts(commands.iterator)
   }