# 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 =