# HG changeset patch # User wenzelm # Date 1373491528 -7200 # Node ID 5cad4a5f5615bb0cf7fdd08d2f7276ce298218a8 # Parent 0a7240d88e0922e57a1983e05a83595cf40d37c8 more abstract message channel; diff -r 0a7240d88e09 -r 5cad4a5f5615 src/Pure/ROOT --- a/src/Pure/ROOT Wed Jul 10 22:56:48 2013 +0200 +++ b/src/Pure/ROOT Wed Jul 10 23:25:28 2013 +0200 @@ -181,6 +181,7 @@ "System/isabelle_process.ML" "System/isabelle_system.ML" "System/isar.ML" + "System/message_channel.ML" "System/options.ML" "System/session.ML" "System/system_channel.ML" diff -r 0a7240d88e09 -r 5cad4a5f5615 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Jul 10 22:56:48 2013 +0200 +++ b/src/Pure/ROOT.ML Wed Jul 10 23:25:28 2013 +0200 @@ -288,6 +288,7 @@ use "System/session.ML"; use "System/command_line.ML"; use "System/system_channel.ML"; +use "System/message_channel.ML"; use "System/isabelle_process.ML"; use "System/invoke_scala.ML"; use "PIDE/protocol.ML"; diff -r 0a7240d88e09 -r 5cad4a5f5615 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Jul 10 22:56:48 2013 +0200 +++ b/src/Pure/System/isabelle_process.ML Wed Jul 10 23:25:28 2013 +0200 @@ -103,45 +103,13 @@ local fun chunk s = [string_of_int (size s), "\n", s]; -fun flush channel = ignore (try System_Channel.flush channel); -datatype target = - Sync of {send: string list -> unit} | - Async of {send: string list -> bool -> unit, shutdown: unit -> unit}; - -fun message do_flush target name raw_props body = +fun message do_flush msg_channel 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), [])); val msg = chunk header @ chunk body; - in (case target of Sync {send} => send msg | Async {send, ...} => send msg do_flush) end; - -fun message_output mbox channel = - let - fun loop receive = - (case receive mbox of - SOME NONE => flush channel - | SOME (SOME (msg, do_flush)) => - (List.app (fn s => System_Channel.output channel s) msg; - if do_flush then flush channel else (); - loop (Mailbox.receive_timeout (seconds 0.02))) - | NONE => (flush channel; loop (SOME o Mailbox.receive))); - in fn () => loop (SOME o Mailbox.receive) end; - -fun make_target channel = - if Multithreading.available then - let - val mbox = Mailbox.create (); - val thread = Simple_Thread.fork false (message_output mbox channel); - in - Async { - send = fn msg => fn do_flush => Mailbox.send mbox (SOME (msg, do_flush)), - shutdown = fn () => - (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread) - } - end - else - Sync {send = fn msg => (List.app (fn s => System_Channel.output channel s) msg; flush channel)}; + in Message_Channel.send msg_channel msg do_flush end; in @@ -150,12 +118,12 @@ val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); - val target = make_target channel; + val msg_channel = Message_Channel.make channel; fun standard_message opt_serial name body = if body = "" then () else - message false target name + message false msg_channel name ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) (Position.properties_of (Position.thread_data ()))) body; in @@ -170,11 +138,11 @@ (fn s => standard_message (SOME (serial ())) Markup.warningN s); Output.Private_Hooks.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s); - Output.Private_Hooks.protocol_message_fn := message true target Markup.protocolN; + Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN; Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; Output.Private_Hooks.prompt_fn := ignore; - message true target Markup.initN [] (Session.welcome ()); - (case target of Async {shutdown, ...} => shutdown | _ => fn () => ()) + message true msg_channel Markup.initN [] (Session.welcome ()); + msg_channel end; end; @@ -242,10 +210,10 @@ (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); val channel = rendezvous (); - val shutdown_channels = init_channels channel; + val msg_channel = init_channels channel; val _ = Session.init_protocol_handlers (); val _ = loop channel; - in shutdown_channels () end); + in Message_Channel.shutdown msg_channel end); fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); diff -r 0a7240d88e09 -r 5cad4a5f5615 src/Pure/System/message_channel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/message_channel.ML Wed Jul 10 23:25:28 2013 +0200 @@ -0,0 +1,54 @@ +(* Title: Pure/System/message_channel.ML + Author: Makarius + +Preferably asynchronous channel for Isabelle messages. +*) + +signature MESSAGE_CHANNEL = +sig + type T + val send: T -> string list -> bool -> unit + val shutdown: T -> unit + val make: System_Channel.T -> T +end; + +structure Message_Channel: MESSAGE_CHANNEL = +struct + +datatype T = Message_Channel of + {send: string list -> bool -> unit, + shutdown: unit -> unit}; + +fun send (Message_Channel {send, ...}) = send; +fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); + +fun flush channel = ignore (try System_Channel.flush channel); + +fun message_output mbox channel = + let + fun loop receive = + (case receive mbox of + SOME NONE => flush channel + | SOME (SOME (msg, do_flush)) => + (List.app (fn s => System_Channel.output channel s) msg; + if do_flush then flush channel else (); + loop (Mailbox.receive_timeout (seconds 0.02))) + | NONE => (flush channel; loop (SOME o Mailbox.receive))); + in fn () => loop (SOME o Mailbox.receive) end; + +fun make channel = + if Multithreading.available then + let + val mbox = Mailbox.create (); + val thread = Simple_Thread.fork false (message_output mbox channel); + fun send msg do_flush = Mailbox.send mbox (SOME (msg, do_flush)); + fun shutdown () = + (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread); + in Message_Channel {send = send, shutdown = shutdown} end + else + let + fun send msg = (List.app (fn s => System_Channel.output channel s) msg; flush channel); + in Message_Channel {send = fn msg => fn _ => send msg, shutdown = fn () => ()} end; + +end; +