--- a/src/Pure/PIDE/document.scala Tue Aug 31 12:49:40 2010 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 31 13:20:12 2010 +0200
@@ -56,7 +56,7 @@
}
}
- private val block_size = 4096
+ private val block_size = 1024
class Node(val commands: Linear_Set[Command])
{