src/Pure/General/socket_io.ML
changeset 45028 d608dd8cd409
parent 45026 5c0b0d67f9b1
equal deleted inserted replaced
45027:f459e93a038e 45028:d608dd8cd409
     7 *)
     7 *)
     8 
     8 
     9 signature SOCKET_IO =
     9 signature SOCKET_IO =
    10 sig
    10 sig
    11   val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    11   val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
    12   val open_streams: string * int -> BinIO.instream * BinIO.outstream
    12   val open_streams: string -> BinIO.instream * BinIO.outstream
    13 end;
    13 end;
    14 
    14 
    15 structure Socket_IO: SOCKET_IO =
    15 structure Socket_IO: SOCKET_IO =
    16 struct
    16 struct
    17 
    17 
    66         (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    66         (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
    67 
    67 
    68   in (in_stream, out_stream) end;
    68   in (in_stream, out_stream) end;
    69 
    69 
    70 
    70 
    71 fun open_streams (hostname, port) =
    71 fun open_streams socket_name =
    72   let
    72   let
    73     val host =
    73     fun err () = error ("Bad socket name: " ^ quote socket_name);
    74       (case NetHostDB.getByName hostname of
    74     val (host, port) =
    75         NONE => error ("Bad host name: " ^ quote hostname)
    75       (case space_explode ":" socket_name of
    76       | SOME host => host);
    76         [h, p] =>
    77     val addr = INetSock.toAddr (NetHostDB.addr host, port);
    77          (case NetHostDB.getByName h of SOME host => host | NONE => err (),
       
    78           case Int.fromString p of SOME port => port | NONE => err ())
       
    79       | _ => err ());
    78     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    80     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
    79     val _ = Socket.connect (socket, addr);
    81     val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
    80   in make_streams socket end;
    82   in make_streams socket end;
    81 
    83 
    82 end;
    84 end;
    83 
    85