Node.full_index: allow command spans larger than block_size;

--- a/src/Pure/PIDE/document.scala	Tue Aug 31 17:49:45 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 31 19:55:43 2010 +0200
@@ -67,7 +67,7 @@
       var last_stop = 0
       for ((command, start) <- Node.command_starts(commands.iterator)) {
         last_stop = start + command.length
-        if (last_stop + 1 > next_block) {
+        while (last_stop + 1 > next_block) {
           blocks += (command -> start)
           next_block += block_size
         }