diff -r c83cdd300848 -r 1f34f6394383 src/Pure/General/socket_io.ML --- a/src/Pure/General/socket_io.ML Fri Nov 24 21:32:32 2023 +0100 +++ b/src/Pure/General/socket_io.ML Fri Nov 24 21:54:30 2023 +0100 @@ -19,12 +19,14 @@ fun close_permissive socket = Socket.close socket handle OS.SysErr _ => (); +val buffer_size = 65536; + fun make_streams socket_name socket = let val rd = BinPrimIO.RD { name = socket_name, - chunkSize = 4096, + chunkSize = buffer_size, readVec = SOME (fn n => Socket.recvVec (socket, n)), readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)), readVecNB = NONE, @@ -43,7 +45,7 @@ val wr = BinPrimIO.WR { name = socket_name, - chunkSize = 4096, + chunkSize = buffer_size, writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)), writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)), writeVecNB = NONE,