changeset 38885 | 06582837872b |
parent 38882 | e1fb3bbc22ab |
child 38976 | a4a465dc89d9 |
--- 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 }