# HG changeset patch # User wenzelm # Date 1373484097 -7200 # Node ID 36aa39694ab42309076e6fe8917e0e33bbbbe8da # Parent 59bf099448bfad906c0d5438871fabfa7ecde512 fall back on synchronous message output for single-threaded SML/NJ; diff -r 59bf099448bf -r 36aa39694ab4 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Jul 10 21:13:32 2013 +0200 +++ b/src/Pure/System/isabelle_process.ML Wed Jul 10 21:21:37 2013 +0200 @@ -103,30 +103,32 @@ local fun chunk s = [string_of_int (size s), "\n", s]; +fun flush channel = ignore (try System_Channel.flush channel); -fun message do_flush mbox name raw_props body = +datatype target = + Channel of System_Channel.T | + Mailbox of (string list * bool) Mailbox.T; + +fun message do_flush target name raw_props body = let val robust_props = map (pairself YXML.embed_controls) raw_props; val header = YXML.string_of (XML.Elem ((name, robust_props), [])); - in Mailbox.send mbox (chunk header @ chunk body, do_flush) end; - -fun standard_message mbox opt_serial name body = - if body = "" then () - else - message false mbox name - ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) - (Position.properties_of (Position.thread_data ()))) body; + val msg = chunk header @ chunk body; + in + (case target of + Channel channel => (List.app (fn s => System_Channel.output channel s) msg; flush channel) + | Mailbox mbox => Mailbox.send mbox (msg, do_flush)) + end; fun message_output mbox channel = let - fun flush () = ignore (try System_Channel.flush channel); fun loop receive = (case receive mbox of SOME (msg, do_flush) => (List.app (fn s => System_Channel.output channel s) msg; - if do_flush then flush () else (); + if do_flush then flush channel else (); loop (Mailbox.receive_timeout (seconds 0.02))) - | NONE => (flush (); loop (SOME o Mailbox.receive))); + | NONE => (flush channel; loop (SOME o Mailbox.receive))); in fn () => loop (SOME o Mailbox.receive) end; in @@ -136,25 +138,36 @@ val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); - val mbox = Mailbox.create () : (string list * bool) Mailbox.T; - val _ = Simple_Thread.fork false (message_output mbox channel); + val target = + if Multithreading.available then + let + val mbox = Mailbox.create (); + val _ = Simple_Thread.fork false (message_output mbox channel); + in Mailbox mbox end + else Channel channel; + + fun standard_message opt_serial name body = + if body = "" then () + else + message false target name + ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) + (Position.properties_of (Position.thread_data ()))) body; in - Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN; - Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN; - Output.Private_Hooks.result_fn := - (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s); + Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN; + Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN; + Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s); Output.Private_Hooks.writeln_fn := - (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s); + (fn s => standard_message (SOME (serial ())) Markup.writelnN s); Output.Private_Hooks.tracing_fn := - (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s)); + (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s)); Output.Private_Hooks.warning_fn := - (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s); + (fn s => standard_message (SOME (serial ())) Markup.warningN s); Output.Private_Hooks.error_fn := - (fn (i, s) => standard_message mbox (SOME i) Markup.errorN s); - Output.Private_Hooks.protocol_message_fn := message true mbox Markup.protocolN; + (fn (i, s) => standard_message (SOME i) Markup.errorN s); + Output.Private_Hooks.protocol_message_fn := message true target Markup.protocolN; Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; Output.Private_Hooks.prompt_fn := ignore; - message true mbox Markup.initN [] (Session.welcome ()) + message true target Markup.initN [] (Session.welcome ()) end; end;