# HG changeset patch
# User wenzelm
# Date 1700859270 -3600
# Node ID 1f34f6394383d2ab19732811c2fd762bae0c444c
# Parent  c83cdd300848fdccb56dae206e7ebfa33fa6616a
more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);

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,
diff -r c83cdd300848 -r 1f34f6394383 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Fri Nov 24 21:32:32 2023 +0100
+++ b/src/Pure/System/system_channel.scala	Fri Nov 24 21:54:30 2023 +0100
@@ -17,7 +17,7 @@
   def apply(unix_domain: Boolean = false): System_Channel =
     if (unix_domain) new Unix else new Inet
 
-  val buffer_size: Integer = Integer.valueOf(131072)
+  val buffer_size: Integer = Integer.valueOf(65536)
 
   class Inet extends System_Channel(StandardProtocolFamily.INET) {
     server.bind(new InetSocketAddress(Server.localhost, 0), 50)