src/Pure/System/isabelle_process.ML
changeset 40301 bf39a257b3d3
parent 40134 8baded087d34
child 40518 035a27279705
equal deleted inserted replaced
40300:d4487353b3a0 40301:bf39a257b3d3
    79   let
    79   let
    80     fun loop receive =
    80     fun loop receive =
    81       (case receive mbox of
    81       (case receive mbox of
    82         SOME msg =>
    82         SOME msg =>
    83          (List.app (fn s => TextIO.output (out_stream, s)) msg;
    83          (List.app (fn s => TextIO.output (out_stream, s)) msg;
    84           loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
    84           loop (Mailbox.receive_timeout (seconds 0.02)))
    85       | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
    85       | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
    86   in fn () => loop (SOME o Mailbox.receive) end;
    86   in fn () => loop (SOME o Mailbox.receive) end;
    87 
    87 
    88 in
    88 in
    89 
    89 
   163 
   163 
   164 (* init *)
   164 (* init *)
   165 
   165 
   166 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   166 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   167   let
   167   let
   168     val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
   168     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
   169     val _ = Output.raw_stdout Symbol.STX;
   169     val _ = Output.raw_stdout Symbol.STX;
   170 
   170 
   171     val _ = quick_and_dirty := true;  (* FIXME !? *)
   171     val _ = quick_and_dirty := true;  (* FIXME !? *)
   172     val _ = Context.set_thread_data NONE;
   172     val _ = Context.set_thread_data NONE;
   173     val _ = Unsynchronized.change print_mode
   173     val _ = Unsynchronized.change print_mode