# HG changeset patch
# User wenzelm
# Date 1316791434 -7200
# Node ID 11f622794ad6d8cbe5b6909cf2757b2395d434c9
# Parent  9a98c3bc72e49a7e3532b8fa94716f78c6b7634b
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);

diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Pure/General/socket_io.ML
--- 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;
-
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Pure/IsaMakefile
--- 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					\
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Pure/ROOT.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";
 
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Tools/WWW_Find/IsaMakefile
--- 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
 
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Tools/WWW_Find/ROOT.ML
--- 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";
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Tools/WWW_Find/scgi_server.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);
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Tools/WWW_Find/server_socket.ML
--- 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;
-
diff -r 9a98c3bc72e4 -r 11f622794ad6 src/Tools/WWW_Find/socket_util.ML
--- /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;
+