discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
authorwenzelm
Fri Sep 23 17:23:54 2011 +0200 (2011-09-23)
changeset 4506611f622794ad6
parent 45065 9a98c3bc72e4
child 45067 d5156aa8556d
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
src/Pure/General/socket_io.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Tools/WWW_Find/IsaMakefile
src/Tools/WWW_Find/ROOT.ML
src/Tools/WWW_Find/scgi_server.ML
src/Tools/WWW_Find/server_socket.ML
src/Tools/WWW_Find/socket_util.ML
     1.1 --- a/src/Pure/General/socket_io.ML	Fri Sep 23 17:11:08 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,85 +0,0 @@
     1.4 -(*  Title:      Pure/General/socket_io.ML
     1.5 -    Author:     Timothy Bourke, NICTA
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Stream IO over TCP sockets.  Following example 10.2 in "The Standard
     1.9 -ML Basis Library" by Emden R. Gansner and John H. Reppy.
    1.10 -*)
    1.11 -
    1.12 -signature SOCKET_IO =
    1.13 -sig
    1.14 -  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    1.15 -  val open_streams: string -> BinIO.instream * BinIO.outstream
    1.16 -end;
    1.17 -
    1.18 -structure Socket_IO: SOCKET_IO =
    1.19 -struct
    1.20 -
    1.21 -fun make_streams socket =
    1.22 -  let
    1.23 -    val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
    1.24 -    val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
    1.25 -
    1.26 -    val rd =
    1.27 -      BinPrimIO.RD {
    1.28 -        name = name,
    1.29 -        chunkSize = Socket.Ctl.getRCVBUF socket,
    1.30 -        readVec = SOME (fn n => Socket.recvVec (socket, n)),
    1.31 -        readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
    1.32 -        readVecNB = NONE,
    1.33 -        readArrNB = NONE,
    1.34 -        block = NONE,
    1.35 -        canInput = NONE,
    1.36 -        avail = fn () => NONE,
    1.37 -        getPos = NONE,
    1.38 -        setPos = NONE,
    1.39 -        endPos = NONE,
    1.40 -        verifyPos = NONE,
    1.41 -        close = fn () => Socket.close socket,
    1.42 -        ioDesc = NONE
    1.43 -      };
    1.44 -
    1.45 -    val wr =
    1.46 -      BinPrimIO.WR {
    1.47 -        name = name,
    1.48 -        chunkSize = Socket.Ctl.getSNDBUF socket,
    1.49 -        writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
    1.50 -        writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
    1.51 -        writeVecNB = NONE,
    1.52 -        writeArrNB = NONE,
    1.53 -        block = NONE,
    1.54 -        canOutput = NONE,
    1.55 -        getPos = NONE,
    1.56 -        setPos = NONE,
    1.57 -        endPos = NONE,
    1.58 -        verifyPos = NONE,
    1.59 -        close = fn () => Socket.close socket,
    1.60 -        ioDesc = NONE
    1.61 -      };
    1.62 -
    1.63 -    val in_stream =
    1.64 -      BinIO.mkInstream
    1.65 -        (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
    1.66 -
    1.67 -    val out_stream =
    1.68 -      BinIO.mkOutstream
    1.69 -        (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    1.70 -
    1.71 -  in (in_stream, out_stream) end;
    1.72 -
    1.73 -
    1.74 -fun open_streams socket_name =
    1.75 -  let
    1.76 -    fun err () = error ("Bad socket name: " ^ quote socket_name);
    1.77 -    val (host, port) =
    1.78 -      (case space_explode ":" socket_name of
    1.79 -        [h, p] =>
    1.80 -         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    1.81 -          case Int.fromString p of SOME port => port | NONE => err ())
    1.82 -      | _ => err ());
    1.83 -    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    1.84 -    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    1.85 -  in make_streams socket end;
    1.86 -
    1.87 -end;
    1.88 -
     2.1 --- a/src/Pure/IsaMakefile	Fri Sep 23 17:11:08 2011 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Fri Sep 23 17:23:54 2011 +0200
     2.3 @@ -98,7 +98,6 @@
     2.4    General/seq.ML					\
     2.5    General/sha1.ML					\
     2.6    General/sha1_polyml.ML				\
     2.7 -  General/socket_io.ML					\
     2.8    General/source.ML					\
     2.9    General/stack.ML					\
    2.10    General/symbol.ML					\
     3.1 --- a/src/Pure/ROOT.ML	Fri Sep 23 17:11:08 2011 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Fri Sep 23 17:23:54 2011 +0200
     3.3 @@ -57,7 +57,6 @@
     3.4  use "General/path.ML";
     3.5  use "General/url.ML";
     3.6  use "General/file.ML";
     3.7 -use "General/socket_io.ML";
     3.8  use "General/long_name.ML";
     3.9  use "General/binding.ML";
    3.10  
     4.1 --- a/src/Tools/WWW_Find/IsaMakefile	Fri Sep 23 17:11:08 2011 +0200
     4.2 +++ b/src/Tools/WWW_Find/IsaMakefile	Fri Sep 23 17:23:54 2011 +0200
     4.3 @@ -30,7 +30,7 @@
     4.4  
     4.5  $(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML	\
     4.6    html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML	\
     4.7 -  scgi_server.ML server_socket.ML unicode_symbols.ML xhtml.ML		\
     4.8 +  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML		\
     4.9    yxml_find_theorems.ML ROOT.ML
    4.10  	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
    4.11  
     5.1 --- a/src/Tools/WWW_Find/ROOT.ML	Fri Sep 23 17:11:08 2011 +0200
     5.2 +++ b/src/Tools/WWW_Find/ROOT.ML	Fri Sep 23 17:23:54 2011 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4    use "http_status.ML";
     5.5    use "http_util.ML";
     5.6    use "xhtml.ML";
     5.7 -  use "server_socket.ML";
     5.8 +  use "socket_util.ML";
     5.9    use "scgi_req.ML";
    5.10    use "scgi_server.ML";
    5.11    use "echo.ML";
     6.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Fri Sep 23 17:11:08 2011 +0200
     6.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Fri Sep 23 17:23:54 2011 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4  
     6.5  fun server server_prefix port =
     6.6    let
     6.7 -    val passive_sock = Server_Socket.init (SOME "localhost") port;
     6.8 +    val passive_sock = Socket_Util.init_server_socket (SOME "localhost") port;
     6.9  
    6.10      val thread_wait = ConditionVar.conditionVar ();
    6.11      val thread_wait_mutex = Mutex.mutex ();
    6.12 @@ -63,7 +63,7 @@
    6.13        let
    6.14          val (sock, _)= Socket.accept passive_sock;
    6.15  
    6.16 -        val (sin, sout) = Socket_IO.make_streams sock;
    6.17 +        val (sin, sout) = Socket_Util.make_streams sock;
    6.18  
    6.19          fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
    6.20          fun send_log msg = (tracing msg; send msg);
     7.1 --- a/src/Tools/WWW_Find/server_socket.ML	Fri Sep 23 17:11:08 2011 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,33 +0,0 @@
     7.4 -(*  Title:      Tools/WWW_Find/socket_util.ML
     7.5 -    Author:     Timothy Bourke, NICTA
     7.6 -
     7.7 -Server sockets.
     7.8 -*)
     7.9 -
    7.10 -signature SERVER_SOCKET =
    7.11 -sig
    7.12 -  val init: string option -> int -> Socket.passive INetSock.stream_sock
    7.13 -end;
    7.14 -
    7.15 -structure Server_Socket: SERVER_SOCKET =
    7.16 -struct
    7.17 -
    7.18 -fun init opt_host port =
    7.19 -  let
    7.20 -    val sock = INetSock.TCP.socket ();
    7.21 -    val addr =
    7.22 -      (case opt_host of
    7.23 -         NONE => INetSock.any port
    7.24 -       | SOME host =>
    7.25 -           NetHostDB.getByName host
    7.26 -           |> the
    7.27 -           |> NetHostDB.addr
    7.28 -           |> rpair port
    7.29 -           |> INetSock.toAddr
    7.30 -           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
    7.31 -    val _ = Socket.bind (sock, addr);
    7.32 -    val _ = Socket.listen (sock, 5);
    7.33 -  in sock end;
    7.34 -
    7.35 -end;
    7.36 -
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/WWW_Find/socket_util.ML	Fri Sep 23 17:23:54 2011 +0200
     8.3 @@ -0,0 +1,89 @@
     8.4 +(*  Title:      Tools/WWW_Find/socket_util.ML
     8.5 +    Author:     Timothy Bourke, NICTA
     8.6 +
     8.7 +Routines for working with sockets.  Following example 10.2 in "The
     8.8 +Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy.
     8.9 +*)
    8.10 +
    8.11 +signature SOCKET_UTIL =
    8.12 +sig
    8.13 +  val init_server_socket: string option -> int -> Socket.passive INetSock.stream_sock
    8.14 +  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    8.15 +end;
    8.16 +
    8.17 +structure Socket_Util: SOCKET_UTIL =
    8.18 +struct
    8.19 +
    8.20 +fun init_server_socket opt_host port =
    8.21 +  let
    8.22 +    val sock = INetSock.TCP.socket ();
    8.23 +    val addr =
    8.24 +      (case opt_host of
    8.25 +         NONE => INetSock.any port
    8.26 +       | SOME host =>
    8.27 +           NetHostDB.getByName host
    8.28 +           |> the
    8.29 +           |> NetHostDB.addr
    8.30 +           |> rpair port
    8.31 +           |> INetSock.toAddr
    8.32 +           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
    8.33 +    val _ = Socket.bind (sock, addr);
    8.34 +    val _ = Socket.listen (sock, 5);
    8.35 +  in sock end;
    8.36 +
    8.37 +fun make_streams sock =
    8.38 +  let
    8.39 +    val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
    8.40 +
    8.41 +    val sock_name =
    8.42 +      implode [ NetHostDB.toString haddr, ":", string_of_int port ];
    8.43 +
    8.44 +    val rd =
    8.45 +      BinPrimIO.RD {
    8.46 +        name = sock_name,
    8.47 +        chunkSize = Socket.Ctl.getRCVBUF sock,
    8.48 +        readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
    8.49 +        readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
    8.50 +        readVecNB = NONE,
    8.51 +        readArrNB = NONE,
    8.52 +        block = NONE,
    8.53 +        canInput = NONE,
    8.54 +        avail = fn () => NONE,
    8.55 +        getPos = NONE,
    8.56 +        setPos = NONE,
    8.57 +        endPos = NONE,
    8.58 +        verifyPos = NONE,
    8.59 +        close = fn () => Socket.close sock,
    8.60 +        ioDesc = NONE
    8.61 +      };
    8.62 +
    8.63 +    val wr =
    8.64 +      BinPrimIO.WR {
    8.65 +        name = sock_name,
    8.66 +        chunkSize = Socket.Ctl.getSNDBUF sock,
    8.67 +        writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
    8.68 +        writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
    8.69 +        writeVecNB = NONE,
    8.70 +        writeArrNB = NONE,
    8.71 +        block = NONE,
    8.72 +        canOutput = NONE,
    8.73 +        getPos = NONE,
    8.74 +        setPos = NONE,
    8.75 +        endPos = NONE,
    8.76 +        verifyPos = NONE,
    8.77 +        close = fn () => Socket.close sock,
    8.78 +        ioDesc = NONE
    8.79 +      };
    8.80 +
    8.81 +    val in_strm =
    8.82 +      BinIO.mkInstream (
    8.83 +        BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
    8.84 +
    8.85 +    val out_strm =
    8.86 +      BinIO.mkOutstream (
    8.87 +        BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    8.88 +
    8.89 +    in (in_strm, out_strm) end;
    8.90 +
    8.91 +end;
    8.92 +