1.1 --- a/src/Pure/General/socket_io.ML	Wed Oct 16 12:04:38 2013 +0200
     1.2 +++ b/src/Pure/General/socket_io.ML	Wed Oct 16 12:14:35 2013 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4      val rd =
     1.5        BinPrimIO.RD {
     1.6          name = name,
     1.7 -        chunkSize = 4096,
     1.8 +        chunkSize = io_buffer_size,
     1.9          readVec = SOME (fn n => Socket.recvVec (socket, n)),
    1.10          readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
    1.11          readVecNB = NONE,
    1.12 @@ -44,7 +44,7 @@
    1.13      val wr =
    1.14        BinPrimIO.WR {
    1.15          name = name,
    1.16 -        chunkSize = 4096,
    1.17 +        chunkSize = io_buffer_size,
    1.18          writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
    1.19          writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
    1.20          writeVecNB = NONE,

     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:04:38 2013 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Oct 16 12:14:35 2013 +0200
     2.3 @@ -51,6 +51,8 @@
     2.4  val raw_explode = SML90.explode;
     2.5  val implode = SML90.implode;
     2.6  
     2.7 +val io_buffer_size = 4096;
     2.8 +
     2.9  fun quit () = exit 0;
    2.10  
    2.11  

     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 16 12:04:38 2013 +0200
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 16 12:14:35 2013 +0200
     3.3 @@ -3,6 +3,7 @@
     3.4  Compatibility file for Standard ML of New Jersey.
     3.5  *)
     3.6  
     3.7 +val io_buffer_size = 4096;
     3.8  use "ML-Systems/proper_int.ML";
     3.9  
    3.10  exception Interrupt;