1(*  Title:      Pure/System/system_channel.ML
2    Author:     Makarius
3
4Socket-based system channel for inter-process communication.
5*)
6
7signature SYSTEM_CHANNEL =
8sig
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
14  val rendezvous: string -> T
15end;
16
17structure System_Channel: SYSTEM_CHANNEL =
18struct
19
20datatype T = System_Channel of BinIO.instream * BinIO.outstream;
21
22fun input_line (System_Channel (in_stream, _)) =
23  let
24    fun result cs = String.implode (rev (#"\n" :: cs));
25    fun read cs =
26      (case BinIO.input1 in_stream of
27        NONE => if null cs then NONE else SOME (result cs)
28      | SOME b =>
29          (case Byte.byteToChar b of
30            #"\n" => SOME (result cs)
31          | c => read (c :: cs)));
32  in read [] end;
33
34fun inputN (System_Channel (in_stream, _)) n =
35  Byte.bytesToString (BinIO.inputN (in_stream, n));
36
37fun output (System_Channel (_, out_stream)) s =
38  File.output out_stream s;
39
40fun flush (System_Channel (_, out_stream)) =
41  BinIO.flushOut out_stream;
42
43fun rendezvous name =
44  let
45    val (in_stream, out_stream) = Socket_IO.open_streams name;
46    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
47  in System_Channel (in_stream, out_stream) end;
48
49end;
50