# HG changeset patch
# User wenzelm
# Date 1256646877 -3600
# Node ID 0496565527bd29b57bd997322798b22eb4b5eebe
# Parent  e15ce5aeb6d5b28e3db0c739aeaf0dfc4691e379
non-critical output -- ship message in one piece;

diff -r e15ce5aeb6d5 -r 0496565527bd src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Oct 27 13:24:40 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Oct 27 13:34:37 2009 +0100
@@ -61,9 +61,6 @@
         else message_pos ts
     | _ => NONE);
 
-fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
-
 in
 
 fun message _ _ "" = ()
@@ -74,14 +71,16 @@
           Position.properties_of (Position.thread_data ())
           |> Position.default_properties pos;
         val txt = clean_string [Symbol.STX] body;
-      in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
+        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
+      in TextIO.output (out_stream, msg) end;
 
 fun init_message out_stream =
   let
     val pid = (Markup.pidN, process_id ());
     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
     val text = Session.welcome ();
-  in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
+    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
+  in TextIO.output (out_stream, msg) end;
 
 end;