src/Pure/System/isabelle_process.ML
changeset 45029 63144ea111f7
parent 45028 d608dd8cd409
child 45057 86c9b73158a8
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 21 22:18:17 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Sep 22 20:33:08 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    . stdout \002: ML running
     1.5    .. stdin/stdout/stderr freely available (raw ML loop)
     1.6    .. protocol thread initialization
     1.7 -  ... switch to in_fifo/out_fifo channels (rendezvous via open)
     1.8 +  ... rendezvous on system channel
     1.9    ... out_fifo INIT(pid): channels ready
    1.10    ... out_fifo STATUS(keywords)
    1.11    ... out_fifo READY: main loop ready
    1.12 @@ -21,8 +21,8 @@
    1.13    val add_command: string -> (string list -> unit) -> unit
    1.14    val command: string -> string list -> unit
    1.15    val crashes: exn list Synchronized.var
    1.16 +  val init_fifos: string -> string -> unit
    1.17    val init_socket: string -> unit
    1.18 -  val init_fifos: string -> string -> unit
    1.19  end;
    1.20  
    1.21  structure Isabelle_Process: ISABELLE_PROCESS =
    1.22 @@ -80,13 +80,13 @@
    1.23        ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    1.24          (Position.properties_of (Position.thread_data ()))) body;
    1.25  
    1.26 -fun message_output mbox out_stream =
    1.27 +fun message_output mbox channel =
    1.28    let
    1.29 -    fun flush () = ignore (try BinIO.flushOut out_stream);
    1.30 +    fun flush () = ignore (try System_Channel.flush channel);
    1.31      fun loop receive =
    1.32        (case receive mbox of
    1.33          SOME (msg, do_flush) =>
    1.34 -         (List.app (fn s => BinIO.output (out_stream, Byte.stringToBytes s)) msg;
    1.35 +         (List.app (fn s => System_Channel.output channel s) msg;
    1.36            if do_flush then flush () else ();
    1.37            loop (Mailbox.receive_timeout (seconds 0.02)))
    1.38        | NONE => (flush (); loop (SOME o Mailbox.receive)));
    1.39 @@ -94,13 +94,13 @@
    1.40  
    1.41  in
    1.42  
    1.43 -fun setup_channels out_stream =
    1.44 +fun setup_channels channel =
    1.45    let
    1.46      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.47      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.48  
    1.49      val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    1.50 -    val _ = Simple_Thread.fork false (message_output mbox out_stream);
    1.51 +    val _ = Simple_Thread.fork false (message_output mbox channel);
    1.52    in
    1.53      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    1.54      Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    1.55 @@ -127,35 +127,23 @@
    1.56    (Synchronized.change crashes (cons crash);
    1.57      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    1.58  
    1.59 -fun read_line stream =
    1.60 -  let
    1.61 -    val content = String.implode o rev;
    1.62 -    fun read cs =
    1.63 -      (case BinIO.input1 stream of
    1.64 -        NONE => (content cs, null cs)
    1.65 -      | SOME b =>
    1.66 -          (case Byte.byteToChar b of
    1.67 -            #"\n" => (content cs, false)
    1.68 -          | c => read (c :: cs)));
    1.69 -  in case read [] of ("", true) => NONE | (s, _) => SOME s end;
    1.70 -
    1.71 -fun read_chunk stream len =
    1.72 +fun read_chunk channel len =
    1.73    let
    1.74      val n =
    1.75        (case Int.fromString len of
    1.76          SOME n => n
    1.77        | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
    1.78 -    val chunk = Byte.bytesToString (BinIO.inputN (stream, n));
    1.79 +    val chunk = System_Channel.inputN channel n;
    1.80      val m = size chunk;
    1.81    in
    1.82      if m = n then chunk
    1.83      else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
    1.84    end;
    1.85  
    1.86 -fun read_command stream =
    1.87 -  (case read_line stream of
    1.88 +fun read_command channel =
    1.89 +  (case System_Channel.input_line channel of
    1.90      NONE => raise Runtime.TERMINATE
    1.91 -  | SOME line => map (read_chunk stream) (space_explode "," line));
    1.92 +  | SOME line => map (read_chunk channel) (space_explode "," line));
    1.93  
    1.94  fun run_command name args =
    1.95    Runtime.debugging (command name) args
    1.96 @@ -164,21 +152,21 @@
    1.97  
    1.98  in
    1.99  
   1.100 -fun loop stream =
   1.101 +fun loop channel =
   1.102    let val continue =
   1.103 -    (case read_command stream of
   1.104 +    (case read_command channel of
   1.105        [] => (Output.error_msg "Isabelle process: no input"; true)
   1.106      | name :: args => (run_command name args; true))
   1.107      handle Runtime.TERMINATE => false
   1.108        | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
   1.109 -  in if continue then loop stream else () end;
   1.110 +  in if continue then loop channel else () end;
   1.111  
   1.112  end;
   1.113  
   1.114  
   1.115  (* init *)
   1.116  
   1.117 -fun init make_streams = ignore (Simple_Thread.fork false (fn () =>
   1.118 +fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
   1.119    let
   1.120      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
   1.121      val _ = Output.physical_stdout Symbol.STX;
   1.122 @@ -194,18 +182,16 @@
   1.123          (fold (update op =)
   1.124            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
   1.125  
   1.126 -    val (in_stream, out_stream) = make_streams ();
   1.127 -    val _ = setup_channels out_stream;
   1.128 +    val channel = rendezvous ();
   1.129 +    val _ = setup_channels channel;
   1.130  
   1.131      val _ = Keyword.status ();
   1.132      val _ = Thy_Info.status ();
   1.133      val _ = Output.status (Markup.markup Markup.ready "process ready");
   1.134 -  in loop in_stream end));
   1.135 +  in loop channel end));
   1.136  
   1.137 -fun rendezvous fifo1 fifo2 = (BinIO.openIn fifo1, BinIO.openOut fifo2);
   1.138 -fun init_fifos fifo1 fifo2 = init (fn () => rendezvous fifo1 fifo2);
   1.139 -
   1.140 -fun init_socket socket_name = init (fn () => Socket_IO.open_streams socket_name);
   1.141 +fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
   1.142 +fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
   1.143  
   1.144  end;
   1.145