discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
--- a/src/Pure/General/socket_io.ML Fri Sep 23 17:11:08 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: Pure/General/socket_io.ML
- Author: Timothy Bourke, NICTA
- Author: Makarius
-
-Stream IO over TCP sockets. Following example 10.2 in "The Standard
-ML Basis Library" by Emden R. Gansner and John H. Reppy.
-*)
-
-signature SOCKET_IO =
-sig
- val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
- val open_streams: string -> BinIO.instream * BinIO.outstream
-end;
-
-structure Socket_IO: SOCKET_IO =
-struct
-
-fun make_streams socket =
- let
- val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
- val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
-
- val rd =
- BinPrimIO.RD {
- name = name,
- chunkSize = Socket.Ctl.getRCVBUF socket,
- readVec = SOME (fn n => Socket.recvVec (socket, n)),
- readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
- readVecNB = NONE,
- readArrNB = NONE,
- block = NONE,
- canInput = NONE,
- avail = fn () => NONE,
- getPos = NONE,
- setPos = NONE,
- endPos = NONE,
- verifyPos = NONE,
- close = fn () => Socket.close socket,
- ioDesc = NONE
- };
-
- val wr =
- BinPrimIO.WR {
- name = name,
- chunkSize = Socket.Ctl.getSNDBUF socket,
- writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
- writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
- writeVecNB = NONE,
- writeArrNB = NONE,
- block = NONE,
- canOutput = NONE,
- getPos = NONE,
- setPos = NONE,
- endPos = NONE,
- verifyPos = NONE,
- close = fn () => Socket.close socket,
- ioDesc = NONE
- };
-
- val in_stream =
- BinIO.mkInstream
- (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
-
- val out_stream =
- BinIO.mkOutstream
- (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
-
- in (in_stream, out_stream) end;
-
-
-fun open_streams socket_name =
- let
- fun err () = error ("Bad socket name: " ^ quote socket_name);
- val (host, port) =
- (case space_explode ":" socket_name of
- [h, p] =>
- (case NetHostDB.getByName h of SOME host => host | NONE => err (),
- case Int.fromString p of SOME port => port | NONE => err ())
- | _ => err ());
- val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
- val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
- in make_streams socket end;
-
-end;
-
--- a/src/Pure/IsaMakefile Fri Sep 23 17:11:08 2011 +0200
+++ b/src/Pure/IsaMakefile Fri Sep 23 17:23:54 2011 +0200
@@ -98,7 +98,6 @@
General/seq.ML \
General/sha1.ML \
General/sha1_polyml.ML \
- General/socket_io.ML \
General/source.ML \
General/stack.ML \
General/symbol.ML \
--- a/src/Pure/ROOT.ML Fri Sep 23 17:11:08 2011 +0200
+++ b/src/Pure/ROOT.ML Fri Sep 23 17:23:54 2011 +0200
@@ -57,7 +57,6 @@
use "General/path.ML";
use "General/url.ML";
use "General/file.ML";
-use "General/socket_io.ML";
use "General/long_name.ML";
use "General/binding.ML";
--- a/src/Tools/WWW_Find/IsaMakefile Fri Sep 23 17:11:08 2011 +0200
+++ b/src/Tools/WWW_Find/IsaMakefile Fri Sep 23 17:23:54 2011 +0200
@@ -30,7 +30,7 @@
$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
- scgi_server.ML server_socket.ML unicode_symbols.ML xhtml.ML \
+ scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML \
yxml_find_theorems.ML ROOT.ML
@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
--- a/src/Tools/WWW_Find/ROOT.ML Fri Sep 23 17:11:08 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML Fri Sep 23 17:23:54 2011 +0200
@@ -5,7 +5,7 @@
use "http_status.ML";
use "http_util.ML";
use "xhtml.ML";
- use "server_socket.ML";
+ use "socket_util.ML";
use "scgi_req.ML";
use "scgi_server.ML";
use "echo.ML";
--- a/src/Tools/WWW_Find/scgi_server.ML Fri Sep 23 17:11:08 2011 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML Fri Sep 23 17:23:54 2011 +0200
@@ -35,7 +35,7 @@
fun server server_prefix port =
let
- val passive_sock = Server_Socket.init (SOME "localhost") port;
+ val passive_sock = Socket_Util.init_server_socket (SOME "localhost") port;
val thread_wait = ConditionVar.conditionVar ();
val thread_wait_mutex = Mutex.mutex ();
@@ -63,7 +63,7 @@
let
val (sock, _)= Socket.accept passive_sock;
- val (sin, sout) = Socket_IO.make_streams sock;
+ val (sin, sout) = Socket_Util.make_streams sock;
fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
fun send_log msg = (tracing msg; send msg);
--- a/src/Tools/WWW_Find/server_socket.ML Fri Sep 23 17:11:08 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Tools/WWW_Find/socket_util.ML
- Author: Timothy Bourke, NICTA
-
-Server sockets.
-*)
-
-signature SERVER_SOCKET =
-sig
- val init: string option -> int -> Socket.passive INetSock.stream_sock
-end;
-
-structure Server_Socket: SERVER_SOCKET =
-struct
-
-fun init opt_host port =
- let
- val sock = INetSock.TCP.socket ();
- val addr =
- (case opt_host of
- NONE => INetSock.any port
- | SOME host =>
- NetHostDB.getByName host
- |> the
- |> NetHostDB.addr
- |> rpair port
- |> INetSock.toAddr
- handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
- val _ = Socket.bind (sock, addr);
- val _ = Socket.listen (sock, 5);
- in sock end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/socket_util.ML Fri Sep 23 17:23:54 2011 +0200
@@ -0,0 +1,89 @@
+(* Title: Tools/WWW_Find/socket_util.ML
+ Author: Timothy Bourke, NICTA
+
+Routines for working with sockets. Following example 10.2 in "The
+Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy.
+*)
+
+signature SOCKET_UTIL =
+sig
+ val init_server_socket: string option -> int -> Socket.passive INetSock.stream_sock
+ val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
+end;
+
+structure Socket_Util: SOCKET_UTIL =
+struct
+
+fun init_server_socket opt_host port =
+ let
+ val sock = INetSock.TCP.socket ();
+ val addr =
+ (case opt_host of
+ NONE => INetSock.any port
+ | SOME host =>
+ NetHostDB.getByName host
+ |> the
+ |> NetHostDB.addr
+ |> rpair port
+ |> INetSock.toAddr
+ handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
+ val _ = Socket.bind (sock, addr);
+ val _ = Socket.listen (sock, 5);
+ in sock end;
+
+fun make_streams sock =
+ let
+ val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
+
+ val sock_name =
+ implode [ NetHostDB.toString haddr, ":", string_of_int port ];
+
+ val rd =
+ BinPrimIO.RD {
+ name = sock_name,
+ chunkSize = Socket.Ctl.getRCVBUF sock,
+ readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
+ readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
+ readVecNB = NONE,
+ readArrNB = NONE,
+ block = NONE,
+ canInput = NONE,
+ avail = fn () => NONE,
+ getPos = NONE,
+ setPos = NONE,
+ endPos = NONE,
+ verifyPos = NONE,
+ close = fn () => Socket.close sock,
+ ioDesc = NONE
+ };
+
+ val wr =
+ BinPrimIO.WR {
+ name = sock_name,
+ chunkSize = Socket.Ctl.getSNDBUF sock,
+ writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
+ writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
+ writeVecNB = NONE,
+ writeArrNB = NONE,
+ block = NONE,
+ canOutput = NONE,
+ getPos = NONE,
+ setPos = NONE,
+ endPos = NONE,
+ verifyPos = NONE,
+ close = fn () => Socket.close sock,
+ ioDesc = NONE
+ };
+
+ val in_strm =
+ BinIO.mkInstream (
+ BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
+
+ val out_strm =
+ BinIO.mkOutstream (
+ BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
+
+ in (in_strm, out_strm) end;
+
+end;
+