# HG changeset patch # User wenzelm # Date 1381918475 -7200 # Node ID fbcaa9f08879dc41d0cd38b6329e70bd602aa2f5 # Parent e1c275df552230e92b878a60f6f612cf6d9b9031 avoid non-portable int constant -- make SML/NJ happy; diff -r e1c275df5522 -r fbcaa9f08879 src/Pure/General/socket_io.ML --- a/src/Pure/General/socket_io.ML Wed Oct 16 12:04:38 2013 +0200 +++ b/src/Pure/General/socket_io.ML Wed Oct 16 12:14:35 2013 +0200 @@ -25,7 +25,7 @@ val rd = BinPrimIO.RD { name = name, - chunkSize = 4096, + chunkSize = io_buffer_size, 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 = 4096, + chunkSize = io_buffer_size, writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)), writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)), writeVecNB = NONE, diff -r e1c275df5522 -r fbcaa9f08879 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Oct 16 12:04:38 2013 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Wed Oct 16 12:14:35 2013 +0200 @@ -51,6 +51,8 @@ val raw_explode = SML90.explode; val implode = SML90.implode; +val io_buffer_size = 4096; + fun quit () = exit 0; diff -r e1c275df5522 -r fbcaa9f08879 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed Oct 16 12:04:38 2013 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Oct 16 12:14:35 2013 +0200 @@ -3,6 +3,7 @@ Compatibility file for Standard ML of New Jersey. *) +val io_buffer_size = 4096; use "ML-Systems/proper_int.ML"; exception Interrupt;