# HG changeset patch
# User wenzelm
# Date 1316620225 -7200
# Node ID 5c0b0d67f9b15142ffe72ccf22e61efa02e0fb5c
# Parent  33a1af99b3a2e4d5aadf4b24f4dbaa9a25f94ce1
slightly more general Socket_IO as part of Pure;

diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Pure/General/socket_io.ML
--- /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;
+
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Pure/IsaMakefile
--- 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					\
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Pure/ROOT.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";
 
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Tools/WWW_Find/IsaMakefile
--- 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
 
 
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Tools/WWW_Find/ROOT.ML
--- 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";
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Tools/WWW_Find/scgi_server.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);
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Tools/WWW_Find/server_socket.ML
--- /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;
+
diff -r 33a1af99b3a2 -r 5c0b0d67f9b1 src/Tools/WWW_Find/socket_util.ML
--- 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;
-