# HG changeset patch
# User wenzelm
# Date 1396600913 -7200
# Node ID 15d0821c86672d6787aafc32f5f9819573a34385
# Parent  91a8561a8e358a81ff19a067b0470e9efad3ec5f
afford larger full_index, to save a few milliseconds during rendering (notably text_overview);

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])