author | wenzelm |
Fri, 13 Sep 2024 19:13:53 +0200 | |
changeset 80877 | e55723709fab |
parent 80876 | 55b74d63b18c |
child 80878 | cddd64134b49 |
--- 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*)}