author | wenzelm |
Thu, 18 May 2017 14:14:20 +0200 | |
changeset 65865 | 177b90f33f40 |
parent 62501 | 98fa1f9a292f |
child 69440 | eaf66384cfe8 |
permissions | -rw-r--r-- |
45029 | 1 |
(* Title: Pure/System/system_channel.ML |
2 |
Author: Makarius |
|
3 |
||
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
4 |
Socket-based system channel for inter-process communication. |
45029 | 5 |
*) |
6 |
||
7 |
signature SYSTEM_CHANNEL = |
|
8 |
sig |
|
9 |
type T |
|
10 |
val input_line: T -> string option |
|
11 |
val inputN: T -> int -> string |
|
12 |
val output: T -> string -> unit |
|
13 |
val flush: T -> unit |
|
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
14 |
val rendezvous: string -> T |
45029 | 15 |
end; |
16 |
||
17 |
structure System_Channel: SYSTEM_CHANNEL = |
|
18 |
struct |
|
19 |
||
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
20 |
datatype T = System_Channel of BinIO.instream * BinIO.outstream; |
45029 | 21 |
|
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
22 |
fun input_line (System_Channel (in_stream, _)) = |
45029 | 23 |
let |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
24 |
fun result cs = String.implode (rev (#"\n" :: cs)); |
45029 | 25 |
fun read cs = |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
26 |
(case BinIO.input1 in_stream of |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
27 |
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
|
28 |
| SOME b => |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
29 |
(case Byte.byteToChar b of |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
30 |
#"\n" => SOME (result cs) |
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
31 |
| c => read (c :: cs))); |
45029 | 32 |
in read [] end; |
33 |
||
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
34 |
fun inputN (System_Channel (in_stream, _)) n = |
62501 | 35 |
Byte.bytesToString (BinIO.inputN (in_stream, n)); |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
36 |
|
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
37 |
fun output (System_Channel (_, out_stream)) s = |
60982
67e389f67073
precise BinIO, without newline conversion on Windows;
wenzelm
parents:
59350
diff
changeset
|
38 |
File.output out_stream s; |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
39 |
|
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
40 |
fun flush (System_Channel (_, out_stream)) = |
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
41 |
BinIO.flushOut out_stream; |
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
42 |
|
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
43 |
fun rendezvous name = |
45029 | 44 |
let |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
45158
diff
changeset
|
45 |
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
|
46 |
val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
54345
diff
changeset
|
47 |
in System_Channel (in_stream, out_stream) end; |
45029 | 48 |
|
49 |
end; |