src/Pure/System/isabelle_process.ML
changeset 45028 d608dd8cd409
parent 44988 33aa6da101d8
child 45029 63144ea111f7
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 21 20:35:50 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Sep 21 22:18:17 2011 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4    val add_command: string -> (string list -> unit) -> unit
     1.5    val command: string -> string list -> unit
     1.6    val crashes: exn list Synchronized.var
     1.7 -  val init: string -> string -> unit
     1.8 +  val init_socket: string -> unit
     1.9 +  val init_fifos: string -> string -> unit
    1.10  end;
    1.11  
    1.12  structure Isabelle_Process: ISABELLE_PROCESS =
    1.13 @@ -81,11 +82,11 @@
    1.14  
    1.15  fun message_output mbox out_stream =
    1.16    let
    1.17 -    fun flush () = ignore (try TextIO.flushOut out_stream);
    1.18 +    fun flush () = ignore (try BinIO.flushOut out_stream);
    1.19      fun loop receive =
    1.20        (case receive mbox of
    1.21          SOME (msg, do_flush) =>
    1.22 -         (List.app (fn s => TextIO.output (out_stream, s)) msg;
    1.23 +         (List.app (fn s => BinIO.output (out_stream, Byte.stringToBytes s)) msg;
    1.24            if do_flush then flush () else ();
    1.25            loop (Mailbox.receive_timeout (seconds 0.02)))
    1.26        | NONE => (flush (); loop (SOME o Mailbox.receive)));
    1.27 @@ -93,12 +94,8 @@
    1.28  
    1.29  in
    1.30  
    1.31 -fun setup_channels in_fifo out_fifo =
    1.32 +fun setup_channels out_stream =
    1.33    let
    1.34 -    (*rendezvous*)
    1.35 -    val in_stream = TextIO.openIn in_fifo;
    1.36 -    val out_stream = TextIO.openOut out_fifo;
    1.37 -
    1.38      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.39      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.40  
    1.41 @@ -114,8 +111,7 @@
    1.42      Output.Private_Hooks.raw_message_fn := message true mbox "H";
    1.43      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.44      Output.Private_Hooks.prompt_fn := ignore;
    1.45 -    message true mbox "A" [] (Session.welcome ());
    1.46 -    in_stream
    1.47 +    message true mbox "A" [] (Session.welcome ())
    1.48    end;
    1.49  
    1.50  end;
    1.51 @@ -131,13 +127,25 @@
    1.52    (Synchronized.change crashes (cons crash);
    1.53      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    1.54  
    1.55 +fun read_line stream =
    1.56 +  let
    1.57 +    val content = String.implode o rev;
    1.58 +    fun read cs =
    1.59 +      (case BinIO.input1 stream of
    1.60 +        NONE => (content cs, null cs)
    1.61 +      | SOME b =>
    1.62 +          (case Byte.byteToChar b of
    1.63 +            #"\n" => (content cs, false)
    1.64 +          | c => read (c :: cs)));
    1.65 +  in case read [] of ("", true) => NONE | (s, _) => SOME s end;
    1.66 +
    1.67  fun read_chunk stream len =
    1.68    let
    1.69      val n =
    1.70        (case Int.fromString len of
    1.71          SOME n => n
    1.72        | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
    1.73 -    val chunk = TextIO.inputN (stream, n);
    1.74 +    val chunk = Byte.bytesToString (BinIO.inputN (stream, n));
    1.75      val m = size chunk;
    1.76    in
    1.77      if m = n then chunk
    1.78 @@ -145,7 +153,7 @@
    1.79    end;
    1.80  
    1.81  fun read_command stream =
    1.82 -  (case TextIO.inputLine stream of
    1.83 +  (case read_line stream of
    1.84      NONE => raise Runtime.TERMINATE
    1.85    | SOME line => map (read_chunk stream) (space_explode "," line));
    1.86  
    1.87 @@ -170,7 +178,7 @@
    1.88  
    1.89  (* init *)
    1.90  
    1.91 -fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
    1.92 +fun init make_streams = ignore (Simple_Thread.fork false (fn () =>
    1.93    let
    1.94      val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
    1.95      val _ = Output.physical_stdout Symbol.STX;
    1.96 @@ -186,11 +194,18 @@
    1.97          (fold (update op =)
    1.98            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
    1.99  
   1.100 -    val in_stream = setup_channels in_fifo out_fifo;
   1.101 +    val (in_stream, out_stream) = make_streams ();
   1.102 +    val _ = setup_channels out_stream;
   1.103 +
   1.104      val _ = Keyword.status ();
   1.105      val _ = Thy_Info.status ();
   1.106      val _ = Output.status (Markup.markup Markup.ready "process ready");
   1.107    in loop in_stream end));
   1.108  
   1.109 +fun rendezvous fifo1 fifo2 = (BinIO.openIn fifo1, BinIO.openOut fifo2);
   1.110 +fun init_fifos fifo1 fifo2 = init (fn () => rendezvous fifo1 fifo2);
   1.111 +
   1.112 +fun init_socket socket_name = init (fn () => Socket_IO.open_streams socket_name);
   1.113 +
   1.114  end;
   1.115