| author | traytel | 
| Sun, 09 Mar 2014 21:40:41 +0100 | |
| changeset 56012 | 158dc03db8be | 
| parent 51930 | 52fd62618631 | 
| permissions | -rw-r--r-- | 
| 45066 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 1 | (* Title: Tools/WWW_Find/socket_util.ML | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 2 | Author: Timothy Bourke, NICTA | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 3 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 4 | Routines for working with sockets. Following example 10.2 in "The | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 5 | Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy. | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 6 | *) | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 7 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 8 | signature SOCKET_UTIL = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 9 | sig | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 10 | val init_server_socket: string option -> int -> Socket.passive INetSock.stream_sock | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 11 | val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 12 | end; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 13 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 14 | structure Socket_Util: SOCKET_UTIL = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 15 | struct | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 16 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 17 | fun init_server_socket opt_host port = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 18 | let | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 19 | val sock = INetSock.TCP.socket (); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 20 | val addr = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 21 | (case opt_host of | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 22 | NONE => INetSock.any port | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 23 | | SOME host => | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 24 | NetHostDB.getByName host | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 25 | |> the | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 26 | |> NetHostDB.addr | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 27 | |> rpair port | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 28 | |> INetSock.toAddr | 
| 51930 
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
 wenzelm parents: 
45066diff
changeset | 29 |            handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host));
 | 
| 45066 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 30 | val _ = Socket.bind (sock, addr); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 31 | val _ = Socket.listen (sock, 5); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 32 | in sock end; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 33 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 34 | fun make_streams sock = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 35 | let | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 36 | val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 37 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 38 | val sock_name = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 39 | implode [ NetHostDB.toString haddr, ":", string_of_int port ]; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 40 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 41 | val rd = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 42 |       BinPrimIO.RD {
 | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 43 | name = sock_name, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 44 | chunkSize = Socket.Ctl.getRCVBUF sock, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 45 | readVec = SOME (fn sz => Socket.recvVec (sock, sz)), | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 46 | readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)), | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 47 | readVecNB = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 48 | readArrNB = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 49 | block = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 50 | canInput = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 51 | avail = fn () => NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 52 | getPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 53 | setPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 54 | endPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 55 | verifyPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 56 | close = fn () => Socket.close sock, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 57 | ioDesc = NONE | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 58 | }; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 59 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 60 | val wr = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 61 |       BinPrimIO.WR {
 | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 62 | name = sock_name, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 63 | chunkSize = Socket.Ctl.getSNDBUF sock, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 64 | writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)), | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 65 | writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)), | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 66 | writeVecNB = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 67 | writeArrNB = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 68 | block = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 69 | canOutput = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 70 | getPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 71 | setPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 72 | endPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 73 | verifyPos = NONE, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 74 | close = fn () => Socket.close sock, | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 75 | ioDesc = NONE | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 76 | }; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 77 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 78 | val in_strm = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 79 | BinIO.mkInstream ( | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 80 | BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList [])); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 81 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 82 | val out_strm = | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 83 | BinIO.mkOutstream ( | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 84 | BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF)); | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 85 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 86 | in (in_strm, out_strm) end; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 87 | |
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 88 | end; | 
| 
11f622794ad6
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
 wenzelm parents: diff
changeset | 89 |