# HG changeset patch # User wenzelm # Date 1283251780 -7200 # Node ID dde403450419e493db4e938d41443fbc8fca59fb # Parent 1d5b3175fd300159c89d625cd030d4ff33817827 Document.Node: significant speedup of command_range etc. via lazy full_index; diff -r 1d5b3175fd30 -r dde403450419 src/Pure/PIDE/document.scala --- 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) }