less ambitious Bytes.chunk_size for potentially more stable Poly/ML GC (see f0d8f659b19a, but also java.io.InputStream.DEFAULT_BUFFER_SIZE);
authorwenzelm
Fri, 13 Sep 2024 19:13:53 +0200
changeset 80877 e55723709fab
parent 80876 55b74d63b18c
child 80878 cddd64134b49
less ambitious Bytes.chunk_size for potentially more stable Poly/ML GC (see f0d8f659b19a, but also java.io.InputStream.DEFAULT_BUFFER_SIZE);
src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Thu Sep 12 20:15:28 2024 +0200
+++ b/src/Pure/General/bytes.ML	Fri Sep 13 19:13:53 2024 +0200
@@ -48,7 +48,7 @@
 
 (* primitive operations *)
 
-val chunk_size = 65000;
+val chunk_size = 16384;
 
 abstype T = Bytes of
   {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}