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