# HG changeset patch
# User wenzelm
# Date 1218569287 -7200
# Node ID 86f0f91471d0a016c75454a1139944b830e2c102
# Parent  0bd68bf0cbb86c90d8c82b723c0fcb5aa24a2beb
message: ignored if body empty;

diff -r 0bd68bf0cbb8 -r 86f0f91471d0 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Tue Aug 12 21:28:05 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Tue Aug 12 21:28:07 2008 +0200
@@ -79,16 +79,17 @@
 
 in
 
-fun message ch body =
-  let
-    val (txt, pos) =
-      let val ts = YXML.parse_body body
-      in (message_text ts, the_default Position.none (message_pos ts)) end
-      handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none);
-    val props =
-      Position.properties_of (Position.thread_data ())
-      |> Position.default_properties pos;
-  in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
+fun message _ "" = ()
+  | message ch body =
+      let
+        val (txt, pos) =
+          let val ts = YXML.parse_body body
+          in (message_text ts, the_default Position.none (message_pos ts)) end
+          handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none);
+        val props =
+          Position.properties_of (Position.thread_data ())
+          |> Position.default_properties pos;
+      in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
 
 fun init_message () =
   let