# HG changeset patch
# User wenzelm
# Date 1381916104 -7200
# Node ID 26c790a6ce435f4b6d17ed4f0d2bfd4ec45ddc58
# Parent  7518a89965febdd5f7c3a44240a5d425ebbf7c97
basic IO buffer size like for fifo -- imitate implicit flushing behaviour more closely;

diff -r 7518a89965fe -r 26c790a6ce43 src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Mon Oct 14 15:46:35 2013 +0200
+++ b/src/Pure/General/socket_io.ML	Wed Oct 16 11:35:04 2013 +0200
@@ -25,7 +25,7 @@
     val rd =
       BinPrimIO.RD {
         name = name,
-        chunkSize = Socket.Ctl.getRCVBUF socket,
+        chunkSize = 4096,
         readVec = SOME (fn n => Socket.recvVec (socket, n)),
         readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
         readVecNB = NONE,
@@ -44,7 +44,7 @@
     val wr =
       BinPrimIO.WR {
         name = name,
-        chunkSize = Socket.Ctl.getSNDBUF socket,
+        chunkSize = 4096,
         writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
         writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
         writeVecNB = NONE,