src/Pure/System/isabelle_process.ML
changeset 52580 36aa39694ab4
parent 52578 bd94e26e4388
child 52582 31467a4b1466
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 21:13:32 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 21:21:37 2013 +0200
     1.3 @@ -103,30 +103,32 @@
     1.4  local
     1.5  
     1.6  fun chunk s = [string_of_int (size s), "\n", s];
     1.7 +fun flush channel = ignore (try System_Channel.flush channel);
     1.8  
     1.9 -fun message do_flush mbox name raw_props body =
    1.10 +datatype target =
    1.11 +  Channel of System_Channel.T |
    1.12 +  Mailbox of (string list * bool) Mailbox.T;
    1.13 +
    1.14 +fun message do_flush target name raw_props body =
    1.15    let
    1.16      val robust_props = map (pairself YXML.embed_controls) raw_props;
    1.17      val header = YXML.string_of (XML.Elem ((name, robust_props), []));
    1.18 -  in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
    1.19 -
    1.20 -fun standard_message mbox opt_serial name body =
    1.21 -  if body = "" then ()
    1.22 -  else
    1.23 -    message false mbox name
    1.24 -      ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    1.25 -        (Position.properties_of (Position.thread_data ()))) body;
    1.26 +    val msg = chunk header @ chunk body;
    1.27 +  in
    1.28 +    (case target of
    1.29 +      Channel channel => (List.app (fn s => System_Channel.output channel s) msg; flush channel)
    1.30 +    | Mailbox mbox => Mailbox.send mbox (msg, do_flush))
    1.31 +  end;
    1.32  
    1.33  fun message_output mbox channel =
    1.34    let
    1.35 -    fun flush () = ignore (try System_Channel.flush channel);
    1.36      fun loop receive =
    1.37        (case receive mbox of
    1.38          SOME (msg, do_flush) =>
    1.39           (List.app (fn s => System_Channel.output channel s) msg;
    1.40 -          if do_flush then flush () else ();
    1.41 +          if do_flush then flush channel else ();
    1.42            loop (Mailbox.receive_timeout (seconds 0.02)))
    1.43 -      | NONE => (flush (); loop (SOME o Mailbox.receive)));
    1.44 +      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
    1.45    in fn () => loop (SOME o Mailbox.receive) end;
    1.46  
    1.47  in
    1.48 @@ -136,25 +138,36 @@
    1.49      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    1.50      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    1.51  
    1.52 -    val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    1.53 -    val _ = Simple_Thread.fork false (message_output mbox channel);
    1.54 +    val target =
    1.55 +      if Multithreading.available then
    1.56 +        let
    1.57 +          val mbox = Mailbox.create ();
    1.58 +          val _ = Simple_Thread.fork false (message_output mbox channel);
    1.59 +        in Mailbox mbox end
    1.60 +      else Channel channel;
    1.61 +
    1.62 +    fun standard_message opt_serial name body =
    1.63 +      if body = "" then ()
    1.64 +      else
    1.65 +        message false target name
    1.66 +          ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
    1.67 +            (Position.properties_of (Position.thread_data ()))) body;
    1.68    in
    1.69 -    Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
    1.70 -    Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
    1.71 -    Output.Private_Hooks.result_fn :=
    1.72 -      (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s);
    1.73 +    Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
    1.74 +    Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
    1.75 +    Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
    1.76      Output.Private_Hooks.writeln_fn :=
    1.77 -      (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
    1.78 +      (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
    1.79      Output.Private_Hooks.tracing_fn :=
    1.80 -      (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s));
    1.81 +      (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
    1.82      Output.Private_Hooks.warning_fn :=
    1.83 -      (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
    1.84 +      (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    1.85      Output.Private_Hooks.error_fn :=
    1.86 -      (fn (i, s) => standard_message mbox (SOME i) Markup.errorN s);
    1.87 -    Output.Private_Hooks.protocol_message_fn := message true mbox Markup.protocolN;
    1.88 +      (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    1.89 +    Output.Private_Hooks.protocol_message_fn := message true target Markup.protocolN;
    1.90      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    1.91      Output.Private_Hooks.prompt_fn := ignore;
    1.92 -    message true mbox Markup.initN [] (Session.welcome ())
    1.93 +    message true target Markup.initN [] (Session.welcome ())
    1.94    end;
    1.95  
    1.96  end;