# HG changeset patch
# User wenzelm
# Date 1283277343 -7200
# Node ID 06582837872b03452e482334dc4860eea6723376
# Parent  9ec5f6010d6e2ce7e34d79f7b65ce136024a9f5f
Node.full_index: allow command spans larger than block_size;

diff -r 9ec5f6010d6e -r 06582837872b src/Pure/PIDE/document.scala
--- 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
         }