--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/socket_io.ML Wed Sep 21 17:50:25 2011 +0200
@@ -0,0 +1,83 @@
+(* 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 * int -> 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 (hostname, port) =
+ let
+ val host =
+ (case NetHostDB.getByName hostname of
+ NONE => error ("Bad host name: " ^ quote hostname)
+ | SOME host => host);
+ val addr = INetSock.toAddr (NetHostDB.addr host, port);
+ val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
+ val _ = Socket.connect (socket, addr);
+ in make_streams socket end;
+
+end;
+
--- a/src/Pure/IsaMakefile Wed Sep 21 16:04:29 2011 +0200
+++ b/src/Pure/IsaMakefile Wed Sep 21 17:50:25 2011 +0200
@@ -98,6 +98,7 @@
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 Wed Sep 21 16:04:29 2011 +0200
+++ b/src/Pure/ROOT.ML Wed Sep 21 17:50:25 2011 +0200
@@ -57,6 +57,7 @@
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 Wed Sep 21 16:04:29 2011 +0200
+++ b/src/Tools/WWW_Find/IsaMakefile Wed Sep 21 17:50:25 2011 +0200
@@ -28,10 +28,10 @@
Pure:
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
-$(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 socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
- ROOT.ML
+$(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 \
+ yxml_find_theorems.ML ROOT.ML
@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
--- a/src/Tools/WWW_Find/ROOT.ML Wed Sep 21 16:04:29 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML Wed Sep 21 17:50:25 2011 +0200
@@ -5,7 +5,7 @@
use "http_status.ML";
use "http_util.ML";
use "xhtml.ML";
- use "socket_util.ML";
+ use "server_socket.ML";
use "scgi_req.ML";
use "scgi_server.ML";
use "echo.ML";
--- a/src/Tools/WWW_Find/scgi_server.ML Wed Sep 21 16:04:29 2011 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML Wed Sep 21 17:50:25 2011 +0200
@@ -35,7 +35,7 @@
fun server server_prefix port =
let
- val passive_sock = SocketUtil.init_server_socket (SOME "localhost") port;
+ val passive_sock = Server_Socket.init (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) = SocketUtil.make_streams sock;
+ val (sin, sout) = Socket_IO.make_streams sock;
fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
fun send_log msg = (tracing msg; send msg);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/server_socket.ML Wed Sep 21 17:50:25 2011 +0200
@@ -0,0 +1,33 @@
+(* 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;
+
--- a/src/Tools/WWW_Find/socket_util.ML Wed Sep 21 16:04:29 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: Tools/WWW_Find/socket_util.ML
- Author: Emden R. Gansner and John H. Reppy
- SML Basis Library, section 10
-
-Routines for working with sockets.
-*)
-
-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 SocketUtil =
-struct
-
-fun init_server_socket hosto port =
- let
- val sock = INetSock.TCP.socket ();
- val addr =
- (case hosto 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));
- in
- Socket.bind (sock, addr);
- Socket.listen (sock, 5);
- 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;
-