equal
deleted
inserted
replaced
46 structure Bytes: BYTES = |
46 structure Bytes: BYTES = |
47 struct |
47 struct |
48 |
48 |
49 (* primitive operations *) |
49 (* primitive operations *) |
50 |
50 |
51 val chunk_size = 1024 * 1024; |
51 val chunk_size = 1024 * 1024 - 8; |
52 |
52 |
53 abstype T = Bytes of |
53 abstype T = Bytes of |
54 {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} |
54 {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} |
55 with |
55 with |
56 |
56 |