src/Pure/System/isabelle_process.ML
changeset 52583 0a7240d88e09
parent 52582 31467a4b1466
child 52584 5cad4a5f5615
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 22:04:57 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 22:56:48 2013 +0200
     1.3 @@ -106,31 +106,43 @@
     1.4  fun flush channel = ignore (try System_Channel.flush channel);
     1.5  
     1.6  datatype target =
     1.7 -  Channel of System_Channel.T |
     1.8 -  Mailbox of (string list * bool) Mailbox.T;
     1.9 +  Sync of {send: string list -> unit} |
    1.10 +  Async of {send: string list -> bool -> unit, shutdown: unit -> unit};
    1.11  
    1.12  fun message do_flush target name raw_props body =
    1.13    let
    1.14      val robust_props = map (pairself YXML.embed_controls) raw_props;
    1.15      val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    1.16      val msg = chunk header @ chunk body;
    1.17 -  in
    1.18 -    (case target of
    1.19 -      Channel channel => (List.app (fn s => System_Channel.output channel s) msg; flush channel)
    1.20 -    | Mailbox mbox => Mailbox.send mbox (msg, do_flush))
    1.21 -  end;
    1.22 +  in (case target of Sync {send} => send msg | Async {send, ...} => send msg do_flush) end;
    1.23  
    1.24  fun message_output mbox channel =
    1.25    let
    1.26      fun loop receive =
    1.27        (case receive mbox of
    1.28 -        SOME (msg, do_flush) =>
    1.29 +        SOME NONE => flush channel
    1.30 +      | SOME (SOME (msg, do_flush)) =>
    1.31           (List.app (fn s => System_Channel.output channel s) msg;
    1.32            if do_flush then flush channel else ();
    1.33            loop (Mailbox.receive_timeout (seconds 0.02)))
    1.34        | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    1.35    in fn () => loop (SOME o Mailbox.receive) end;
    1.36  
    1.37 +fun make_target channel =
    1.38 +  if Multithreading.available then
    1.39 +    let
    1.40 +      val mbox = Mailbox.create ();
    1.41 +      val thread = Simple_Thread.fork false (message_output mbox channel);
    1.42 +    in
    1.43 +      Async {
    1.44 +        send = fn msg => fn do_flush => Mailbox.send mbox (SOME (msg, do_flush)),
    1.45 +        shutdown = fn () =>
    1.46 +          (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread)
    1.47 +      }
    1.48 +    end
    1.49 +  else
    1.50 +    Sync {send = fn msg => (List.app (fn s => System_Channel.output channel s) msg; flush channel)};
    1.51 +
    1.52  in
    1.53  
    1.54  fun init_channels channel =
    1.55 @@ -138,13 +150,7 @@
    1.56      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.57      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.58  
    1.59 -    val target =
    1.60 -      if Multithreading.available then
    1.61 -        let
    1.62 -          val mbox = Mailbox.create ();
    1.63 -          val _ = Simple_Thread.fork false (message_output mbox channel);
    1.64 -        in Mailbox mbox end
    1.65 -      else Channel channel;
    1.66 +    val target = make_target channel;
    1.67  
    1.68      fun standard_message opt_serial name body =
    1.69        if body = "" then ()
    1.70 @@ -167,7 +173,8 @@
    1.71      Output.Private_Hooks.protocol_message_fn := message true target Markup.protocolN;
    1.72      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.73      Output.Private_Hooks.prompt_fn := ignore;
    1.74 -    message true target Markup.initN [] (Session.welcome ())
    1.75 +    message true target Markup.initN [] (Session.welcome ());
    1.76 +    (case target of Async {shutdown, ...} => shutdown | _ => fn () => ())
    1.77    end;
    1.78  
    1.79  end;
    1.80 @@ -235,9 +242,10 @@
    1.81          (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
    1.82  
    1.83      val channel = rendezvous ();
    1.84 -    val _ = init_channels channel;
    1.85 +    val shutdown_channels = init_channels channel;
    1.86      val _ = Session.init_protocol_handlers ();
    1.87 -  in loop channel end);
    1.88 +    val _ = loop channel;
    1.89 +  in shutdown_channels () end);
    1.90  
    1.91  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
    1.92  fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);