diff -r 91a8561a8e35 -r 15d0821c8667 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Apr 03 22:04:57 2014 +0200 +++ b/src/Pure/PIDE/document.scala Fri Apr 04 10:41:53 2014 +0200 @@ -187,7 +187,7 @@ } } - private val block_size = 1024 + private val block_size = 256 } final class Commands private(val commands: Linear_Set[Command])