author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 45066 | 11f622794ad6 |
child 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 |
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
|
29 |
handle Option => raise Fail ("Cannot resolve hostname: " ^ 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
|
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 |