# HG changeset patch
# User wenzelm
# Date 1618323583 -7200
# Node ID 629868f96c81a6c2ebfe8ac78b1397fe3edf5175
# Parent  6c8fc3c038eb37aeee1b5c5a0dfbfe34559d23e8
misc tuning and clarification;

diff -r 6c8fc3c038eb -r 629868f96c81 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Apr 13 11:44:47 2021 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 13 16:19:43 2021 +0200
@@ -106,7 +106,7 @@
     (* messages *)
 
     val message_channel = Message_Channel.make out_stream;
-    val message = Message_Channel.send_message message_channel;
+    val message = Message_Channel.message message_channel;
 
     fun standard_message props name ss =
       if forall (fn s => s = "") ss then ()
diff -r 6c8fc3c038eb -r 629868f96c81 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Tue Apr 13 11:44:47 2021 +0200
+++ b/src/Pure/System/message_channel.ML	Tue Apr 13 16:19:43 2021 +0200
@@ -7,43 +7,39 @@
 signature MESSAGE_CHANNEL =
 sig
   type T
-  val send_message: T -> string -> Properties.T -> XML.body list -> unit
   val shutdown: T -> unit
+  val message: T -> string -> Properties.T -> XML.body list -> unit
   val make: BinIO.outstream -> T
 end;
 
 structure Message_Channel: MESSAGE_CHANNEL =
 struct
 
-datatype message = Message of XML.body list;
-datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
+datatype message = Shutdown | Message of XML.body list;
+
+datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Thread.thread};
 
-fun send_message (Message_Channel {send, ...}) name raw_props chunks =
+fun shutdown (Message_Channel {mbox, thread}) =
+ (Mailbox.send mbox Shutdown;
+  Mailbox.await_empty mbox;
+  Isabelle_Thread.join thread);
+
+fun message (Message_Channel {mbox, ...}) name raw_props chunks =
   let
     val robust_props = map (apply2 YXML.embed_controls) raw_props;
     val header = [XML.Elem ((name, robust_props), [])];
-  in send (Message (header :: chunks)) end;
-
-fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
-
-fun message_output mbox stream =
-  let
-    fun continue () = Mailbox.receive NONE mbox |> received
-    and received [] = continue ()
-      | received (NONE :: _) = ()
-      | received (SOME (Message chunks) :: rest) =
-          (Byte_Message.write_message_yxml stream chunks; received rest);
-  in continue end;
+  in Mailbox.send mbox (Message (header :: chunks)) end;
 
 fun make stream =
   let
     val mbox = Mailbox.create ();
+    fun loop () = Mailbox.receive NONE mbox |> dispatch
+    and dispatch [] = loop ()
+      | dispatch (Shutdown :: _) = ()
+      | dispatch (Message chunks :: rest) =
+          (Byte_Message.write_message_yxml stream chunks; dispatch rest);
     val thread =
-      Isabelle_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
-        (message_output mbox stream);
-    fun send msg = Mailbox.send mbox (SOME msg);
-    fun shutdown () =
-      (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Isabelle_Thread.join thread);
-  in Message_Channel {send = send, shutdown = shutdown} end;
+      Isabelle_Thread.fork {name = "message_channel", stack_limit = NONE, interrupts = false} loop;
+  in Message_Channel {mbox = mbox, thread = thread} end;
 
 end;