message: ignored if body empty;
authorwenzelm
Tue, 12 Aug 2008 21:28:07 +0200
changeset 27844 86f0f91471d0
parent 27843 0bd68bf0cbb8
child 27845 141772c866c9
message: ignored if body empty;
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