src/Pure/System/isabelle_process.ML
changeset 39528 c01d89d18ff0
parent 39513 fce2202892c4
child 39530 16adc476348f
     1.1 --- a/src/Pure/System/isabelle_process.ML	Sun Sep 19 22:20:48 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Sun Sep 19 22:40:22 2010 +0200
     1.3 @@ -3,6 +3,16 @@
     1.4  
     1.5  Isabelle process wrapper, based on private fifos for maximum
     1.6  robustness and performance.
     1.7 +
     1.8 +Startup phases:
     1.9 +  . raw Posix process startup with uncontrolled output on stdout/stderr
    1.10 +  . stdout \002: ML running
    1.11 +  .. stdin/stdout/stderr freely available (raw ML loop)
    1.12 +  .. protocol thread initialization
    1.13 +  ... switch to in_fifo/out_fifo channels (rendezvous via open)
    1.14 +  ... out_fifo INIT(pid): channels ready
    1.15 +  ... out_fifo STATUS(keywords)
    1.16 +  ... out_fifo READY: main loop ready
    1.17  *)
    1.18  
    1.19  signature ISABELLE_PROCESS =
    1.20 @@ -166,17 +176,21 @@
    1.21  
    1.22  (* init *)
    1.23  
    1.24 -fun init in_fifo out_fifo =
    1.25 +fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
    1.26    let
    1.27 +    val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
    1.28 +    val _ = Output.std_output Symbol.STX;
    1.29 +
    1.30 +    val _ = quick_and_dirty := true;  (* FIXME !? *)
    1.31 +    val _ = Context.set_thread_data NONE;
    1.32      val _ = Unsynchronized.change print_mode
    1.33        (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
    1.34 +
    1.35      val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
    1.36      val _ = init_message out_stream;
    1.37 -    val _ = quick_and_dirty := true;  (* FIXME !? *)
    1.38      val _ = Keyword.status ();
    1.39      val _ = Output.status (Markup.markup Markup.ready "");
    1.40 -    val _ = Context.set_thread_data NONE;
    1.41 -    val _ = Simple_Thread.fork false (fn () => (loop in_stream; quit ()));
    1.42 -  in () end;
    1.43 +  in loop in_stream end));
    1.44  
    1.45  end;
    1.46 +