abstract System_Channel in ML (cf. Scala version);
authorwenzelm
Thu Sep 22 20:33:08 2011 +0200 (2011-09-22)
changeset 4502963144ea111f7
parent 45028 d608dd8cd409
child 45030 9cf265a192f6
abstract System_Channel in ML (cf. Scala version);
back to TextIO for fifo, which is more stable in Poly/ML 5.4.x;
explicit block buffering -- BinIO might be subject to old Poly/ML defaults;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/system_channel.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Sep 21 22:18:17 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Sep 22 20:33:08 2011 +0200
     1.3 @@ -195,6 +195,7 @@
     1.4    System/isabelle_system.ML				\
     1.5    System/isar.ML					\
     1.6    System/session.ML					\
     1.7 +  System/system_channel.ML				\
     1.8    Thy/html.ML						\
     1.9    Thy/latex.ML						\
    1.10    Thy/present.ML					\
     2.1 --- a/src/Pure/ROOT.ML	Wed Sep 21 22:18:17 2011 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Thu Sep 22 20:33:08 2011 +0200
     2.3 @@ -267,6 +267,7 @@
     2.4  (* Isabelle/Isar system *)
     2.5  
     2.6  use "System/session.ML";
     2.7 +use "System/system_channel.ML";
     2.8  use "System/isabelle_process.ML";
     2.9  use "System/invoke_scala.ML";
    2.10  use "PIDE/isar_document.ML";
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 21 22:18:17 2011 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Sep 22 20:33:08 2011 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4    . stdout \002: ML running
     3.5    .. stdin/stdout/stderr freely available (raw ML loop)
     3.6    .. protocol thread initialization
     3.7 -  ... switch to in_fifo/out_fifo channels (rendezvous via open)
     3.8 +  ... rendezvous on system channel
     3.9    ... out_fifo INIT(pid): channels ready
    3.10    ... out_fifo STATUS(keywords)
    3.11    ... out_fifo READY: main loop ready
    3.12 @@ -21,8 +21,8 @@
    3.13    val add_command: string -> (string list -> unit) -> unit
    3.14    val command: string -> string list -> unit
    3.15    val crashes: exn list Synchronized.var
    3.16 +  val init_fifos: string -> string -> unit
    3.17    val init_socket: string -> unit
    3.18 -  val init_fifos: string -> string -> unit
    3.19  end;
    3.20  
    3.21  structure Isabelle_Process: ISABELLE_PROCESS =
    3.22 @@ -80,13 +80,13 @@
    3.23        ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    3.24          (Position.properties_of (Position.thread_data ()))) body;
    3.25  
    3.26 -fun message_output mbox out_stream =
    3.27 +fun message_output mbox channel =
    3.28    let
    3.29 -    fun flush () = ignore (try BinIO.flushOut out_stream);
    3.30 +    fun flush () = ignore (try System_Channel.flush channel);
    3.31      fun loop receive =
    3.32        (case receive mbox of
    3.33          SOME (msg, do_flush) =>
    3.34 -         (List.app (fn s => BinIO.output (out_stream, Byte.stringToBytes s)) msg;
    3.35 +         (List.app (fn s => System_Channel.output channel s) msg;
    3.36            if do_flush then flush () else ();
    3.37            loop (Mailbox.receive_timeout (seconds 0.02)))
    3.38        | NONE => (flush (); loop (SOME o Mailbox.receive)));
    3.39 @@ -94,13 +94,13 @@
    3.40  
    3.41  in
    3.42  
    3.43 -fun setup_channels out_stream =
    3.44 +fun setup_channels channel =
    3.45    let
    3.46      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    3.47      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    3.48  
    3.49      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    3.50 -    val _ = Simple_Thread.fork false (message_output mbox out_stream);
    3.51 +    val _ = Simple_Thread.fork false (message_output mbox channel);
    3.52    in
    3.53      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    3.54      Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    3.55 @@ -127,35 +127,23 @@
    3.56    (Synchronized.change crashes (cons crash);
    3.57      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    3.58  
    3.59 -fun read_line stream =
    3.60 -  let
    3.61 -    val content = String.implode o rev;
    3.62 -    fun read cs =
    3.63 -      (case BinIO.input1 stream of
    3.64 -        NONE => (content cs, null cs)
    3.65 -      | SOME b =>
    3.66 -          (case Byte.byteToChar b of
    3.67 -            #"\n" => (content cs, false)
    3.68 -          | c => read (c :: cs)));
    3.69 -  in case read [] of ("", true) => NONE | (s, _) => SOME s end;
    3.70 -
    3.71 -fun read_chunk stream len =
    3.72 +fun read_chunk channel len =
    3.73    let
    3.74      val n =
    3.75        (case Int.fromString len of
    3.76          SOME n => n
    3.77        | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
    3.78 -    val chunk = Byte.bytesToString (BinIO.inputN (stream, n));
    3.79 +    val chunk = System_Channel.inputN channel n;
    3.80      val m = size chunk;
    3.81    in
    3.82      if m = n then chunk
    3.83      else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
    3.84    end;
    3.85  
    3.86 -fun read_command stream =
    3.87 -  (case read_line stream of
    3.88 +fun read_command channel =
    3.89 +  (case System_Channel.input_line channel of
    3.90      NONE => raise Runtime.TERMINATE
    3.91 -  | SOME line => map (read_chunk stream) (space_explode "," line));
    3.92 +  | SOME line => map (read_chunk channel) (space_explode "," line));
    3.93  
    3.94  fun run_command name args =
    3.95    Runtime.debugging (command name) args
    3.96 @@ -164,21 +152,21 @@
    3.97  
    3.98  in
    3.99  
   3.100 -fun loop stream =
   3.101 +fun loop channel =
   3.102    let val continue =
   3.103 -    (case read_command stream of
   3.104 +    (case read_command channel of
   3.105        [] => (Output.error_msg "Isabelle process: no input"; true)
   3.106      | name :: args => (run_command name args; true))
   3.107      handle Runtime.TERMINATE => false
   3.108        | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
   3.109 -  in if continue then loop stream else () end;
   3.110 +  in if continue then loop channel else () end;
   3.111  
   3.112  end;
   3.113  
   3.114  
   3.115  (* init *)
   3.116  
   3.117 -fun init make_streams = ignore (Simple_Thread.fork false (fn () =>
   3.118 +fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
   3.119    let
   3.120      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
   3.121      val _ = Output.physical_stdout Symbol.STX;
   3.122 @@ -194,18 +182,16 @@
   3.123          (fold (update op =)
   3.124            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
   3.125  
   3.126 -    val (in_stream, out_stream) = make_streams ();
   3.127 -    val _ = setup_channels out_stream;
   3.128 +    val channel = rendezvous ();
   3.129 +    val _ = setup_channels channel;
   3.130  
   3.131      val _ = Keyword.status ();
   3.132      val _ = Thy_Info.status ();
   3.133      val _ = Output.status (Markup.markup Markup.ready "process ready");
   3.134 -  in loop in_stream end));
   3.135 +  in loop channel end));
   3.136  
   3.137 -fun rendezvous fifo1 fifo2 = (BinIO.openIn fifo1, BinIO.openOut fifo2);
   3.138 -fun init_fifos fifo1 fifo2 = init (fn () => rendezvous fifo1 fifo2);
   3.139 -
   3.140 -fun init_socket socket_name = init (fn () => Socket_IO.open_streams socket_name);
   3.141 +fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
   3.142 +fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
   3.143  
   3.144  end;
   3.145  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/System/system_channel.ML	Thu Sep 22 20:33:08 2011 +0200
     4.3 @@ -0,0 +1,77 @@
     4.4 +(*  Title:      Pure/System/system_channel.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Portable system channel for inter-process communication, based on
     4.8 +named pipes or sockets.
     4.9 +*)
    4.10 +
    4.11 +signature SYSTEM_CHANNEL =
    4.12 +sig
    4.13 +  type T
    4.14 +  val input_line: T -> string option
    4.15 +  val inputN: T -> int -> string
    4.16 +  val output: T -> string -> unit
    4.17 +  val flush: T -> unit
    4.18 +  val fifo_rendezvous: string -> string -> T
    4.19 +  val socket_rendezvous: string -> T
    4.20 +end;
    4.21 +
    4.22 +structure System_Channel: SYSTEM_CHANNEL =
    4.23 +struct
    4.24 +
    4.25 +datatype T = System_Channel of
    4.26 + {input_line: unit -> string option,
    4.27 +  inputN: int -> string,
    4.28 +  output: string -> unit,
    4.29 +  flush: unit -> unit};
    4.30 +
    4.31 +fun input_line (System_Channel {input_line = f, ...}) = f ();
    4.32 +fun inputN (System_Channel {inputN = f, ...}) n = f n;
    4.33 +fun output (System_Channel {output = f, ...}) s = f s;
    4.34 +fun flush (System_Channel {flush = f, ...}) = f ();
    4.35 +
    4.36 +
    4.37 +(* named pipes *)
    4.38 +
    4.39 +fun fifo_rendezvous fifo1 fifo2 =
    4.40 +  let
    4.41 +    val in_stream = TextIO.openIn fifo1;
    4.42 +    val out_stream = TextIO.openOut fifo2;
    4.43 +    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF);
    4.44 +  in
    4.45 +    System_Channel
    4.46 +     {input_line = fn () => TextIO.inputLine in_stream,
    4.47 +      inputN = fn n => TextIO.inputN (in_stream, n),
    4.48 +      output = fn s => TextIO.output (out_stream, s),
    4.49 +      flush = fn () => TextIO.flushOut out_stream}
    4.50 +  end;
    4.51 +
    4.52 +
    4.53 +(* sockets *)
    4.54 +
    4.55 +fun read_line in_stream =
    4.56 +  let
    4.57 +    fun result cs = String.implode (rev (#"\n" :: cs));
    4.58 +    fun read cs =
    4.59 +      (case BinIO.input1 in_stream of
    4.60 +        NONE => if null cs then NONE else SOME (result cs)
    4.61 +      | SOME b =>
    4.62 +          (case Byte.byteToChar b of
    4.63 +            #"\n" => SOME (result cs)
    4.64 +          | c => read (c :: cs)));
    4.65 +  in read [] end;
    4.66 +
    4.67 +fun socket_rendezvous name =
    4.68 +  let
    4.69 +    val (in_stream, out_stream) = Socket_IO.open_streams name;
    4.70 +    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
    4.71 +  in
    4.72 +    System_Channel
    4.73 +     {input_line = fn () => read_line in_stream,
    4.74 +      inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
    4.75 +      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
    4.76 +      flush = fn () => BinIO.flushOut out_stream}
    4.77 +  end;
    4.78 +
    4.79 +end;
    4.80 +