src/Pure/General/socket_io.ML
changeset 45028 d608dd8cd409
parent 45026 5c0b0d67f9b1
     1.1 --- a/src/Pure/General/socket_io.ML	Wed Sep 21 20:35:50 2011 +0200
     1.2 +++ b/src/Pure/General/socket_io.ML	Wed Sep 21 22:18:17 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  signature SOCKET_IO =
     1.5  sig
     1.6    val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
     1.7 -  val open_streams: string * int -> BinIO.instream * BinIO.outstream
     1.8 +  val open_streams: string -> BinIO.instream * BinIO.outstream
     1.9  end;
    1.10  
    1.11  structure Socket_IO: SOCKET_IO =
    1.12 @@ -68,15 +68,17 @@
    1.13    in (in_stream, out_stream) end;
    1.14  
    1.15  
    1.16 -fun open_streams (hostname, port) =
    1.17 +fun open_streams socket_name =
    1.18    let
    1.19 -    val host =
    1.20 -      (case NetHostDB.getByName hostname of
    1.21 -        NONE => error ("Bad host name: " ^ quote hostname)
    1.22 -      | SOME host => host);
    1.23 -    val addr = INetSock.toAddr (NetHostDB.addr host, port);
    1.24 +    fun err () = error ("Bad socket name: " ^ quote socket_name);
    1.25 +    val (host, port) =
    1.26 +      (case space_explode ":" socket_name of
    1.27 +        [h, p] =>
    1.28 +         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
    1.29 +          case Int.fromString p of SOME port => port | NONE => err ())
    1.30 +      | _ => err ());
    1.31      val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    1.32 -    val _ = Socket.connect (socket, addr);
    1.33 +    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    1.34    in make_streams socket end;
    1.35  
    1.36  end;