afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
--- 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])