# HG changeset patch # User wenzelm # Date 1618307087 -7200 # Node ID 6c8fc3c038eb37aeee1b5c5a0dfbfe34559d23e8 # Parent b50f8cc8c08e991a5c5dc9db2578203d36706ffb tuned signature; diff -r b50f8cc8c08e -r 6c8fc3c038eb src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Apr 12 22:57:39 2021 +0200 +++ b/src/Pure/System/isabelle_process.ML Tue Apr 13 11:44:47 2021 +0200 @@ -105,10 +105,8 @@ (* messages *) - val msg_channel = Message_Channel.make out_stream; - - fun message name props chunks = - Message_Channel.send msg_channel (Message_Channel.message name props chunks); + val message_channel = Message_Channel.make out_stream; + val message = Message_Channel.send_message message_channel; fun standard_message props name ss = if forall (fn s => s = "") ss then () @@ -178,7 +176,7 @@ val _ = Future.shutdown (); val _ = Execution.reset (); - val _ = Message_Channel.shutdown msg_channel; + val _ = Message_Channel.shutdown message_channel; val _ = BinIO.closeIn in_stream; val _ = BinIO.closeOut out_stream; diff -r b50f8cc8c08e -r 6c8fc3c038eb src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Mon Apr 12 22:57:39 2021 +0200 +++ b/src/Pure/System/message_channel.ML Tue Apr 13 11:44:47 2021 +0200 @@ -6,10 +6,8 @@ signature MESSAGE_CHANNEL = sig - type message - val message: string -> Properties.T -> XML.body list -> message type T - val send: T -> message -> unit + val send_message: T -> string -> Properties.T -> XML.body list -> unit val shutdown: T -> unit val make: BinIO.outstream -> T end; @@ -17,22 +15,15 @@ structure Message_Channel: MESSAGE_CHANNEL = struct -(* message *) +datatype message = Message of XML.body list; +datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; -datatype message = Message of XML.body list; - -fun message name raw_props chunks = +fun send_message (Message_Channel {send, ...}) name raw_props chunks = let val robust_props = map (apply2 YXML.embed_controls) raw_props; val header = [XML.Elem ((name, robust_props), [])]; - in Message (header :: chunks) end; - + in send (Message (header :: chunks)) end; -(* channel *) - -datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; - -fun send (Message_Channel {send, ...}) = send; fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); fun message_output mbox stream =