author | wenzelm |
Thu, 05 Sep 2013 21:37:32 +0200 | |
changeset 53423 | b5a279c7d7f3 |
parent 50800 | c0fb2839d1a9 |
child 54341 | e1c275df5522 |
permissions | -rw-r--r-- |
45029 | 1 |
(* Title: Pure/System/system_channel.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Portable system channel for inter-process communication, based on |
|
5 |
named pipes or sockets. |
|
6 |
*) |
|
7 |
||
8 |
signature SYSTEM_CHANNEL = |
|
9 |
sig |
|
10 |
type T |
|
11 |
val input_line: T -> string option |
|
12 |
val inputN: T -> int -> string |
|
13 |
val output: T -> string -> unit |
|
14 |
val flush: T -> unit |
|
15 |
val fifo_rendezvous: string -> string -> T |
|
16 |
val socket_rendezvous: string -> T |
|
17 |
end; |
|
18 |
||
19 |
structure System_Channel: SYSTEM_CHANNEL = |
|
20 |
struct |
|
21 |
||
22 |
datatype T = System_Channel of |
|
23 |
{input_line: unit -> string option, |
|
24 |
inputN: int -> string, |
|
25 |
output: string -> unit, |
|
26 |
flush: unit -> unit}; |
|
27 |
||
28 |
fun input_line (System_Channel {input_line = f, ...}) = f (); |
|
29 |
fun inputN (System_Channel {inputN = f, ...}) n = f n; |
|
30 |
fun output (System_Channel {output = f, ...}) s = f s; |
|
31 |
fun flush (System_Channel {flush = f, ...}) = f (); |
|
32 |
||
33 |
||
34 |
(* named pipes *) |
|
35 |
||
36 |
fun fifo_rendezvous fifo1 fifo2 = |
|
37 |
let |
|
38 |
val in_stream = TextIO.openIn fifo1; |
|
39 |
val out_stream = TextIO.openOut fifo2; |
|
40 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF); |
|
41 |
in |
|
42 |
System_Channel |
|
43 |
{input_line = fn () => TextIO.inputLine in_stream, |
|
44 |
inputN = fn n => TextIO.inputN (in_stream, n), |
|
45 |
output = fn s => TextIO.output (out_stream, s), |
|
46 |
flush = fn () => TextIO.flushOut out_stream} |
|
47 |
end; |
|
48 |
||
49 |
||
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
50 |
(* sockets *) |
45058
8b20be429cf3
raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
wenzelm
parents:
45029
diff
changeset
|
51 |
|
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
52 |
fun read_line in_stream = |
45029 | 53 |
let |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
54 |
fun result cs = String.implode (rev (#"\n" :: cs)); |
45029 | 55 |
fun read cs = |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
56 |
(case BinIO.input1 in_stream of |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
57 |
NONE => if null cs then NONE else SOME (result cs) |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
58 |
| SOME b => |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
59 |
(case Byte.byteToChar b of |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
60 |
#"\n" => SOME (result cs) |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
61 |
| c => read (c :: cs))); |
45029 | 62 |
in read [] end; |
63 |
||
64 |
fun socket_rendezvous name = |
|
65 |
let |
|
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
66 |
val (in_stream, out_stream) = Socket_IO.open_streams name; |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
67 |
val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); |
45029 | 68 |
in |
69 |
System_Channel |
|
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
70 |
{input_line = fn () => read_line in_stream, |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
71 |
inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)), |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
72 |
output = fn s => BinIO.output (out_stream, Byte.stringToBytes s), |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
73 |
flush = fn () => BinIO.flushOut out_stream} |
45029 | 74 |
end; |
75 |
||
76 |
end; |
|
77 |