src/Pure/System/system_channel.ML
author wenzelm
Mon, 10 Dec 2018 20:20:24 +0100
changeset 69441 0bd51c6aaa8b
parent 69440 eaf66384cfe8
child 69448 51e696887b81
permissions -rw-r--r--
clarified modules, following bytes.scala;

(*  Title:      Pure/System/system_channel.ML
    Author:     Makarius

Socket-based system channel for inter-process communication.
*)

signature SYSTEM_CHANNEL =
sig
  type T
  val input_line: T -> string option
  val inputN: T -> int -> string
  val output: T -> string -> unit
  val flush: T -> unit
  val rendezvous: string -> T
end;

structure System_Channel: SYSTEM_CHANNEL =
struct

datatype T = System_Channel of BinIO.instream * BinIO.outstream;

fun input_line (System_Channel (stream, _)) = Bytes.read_line stream;
fun inputN (System_Channel (stream, _)) n = Bytes.read_block stream n;

fun output (System_Channel (_, stream)) s = File.output stream s;
fun flush (System_Channel (_, stream)) = BinIO.flushOut stream;

fun rendezvous name =
  let
    val (in_stream, out_stream) = Socket_IO.open_streams name;
    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
  in System_Channel (in_stream, out_stream) end;

end;