allow empty body for raw_message -- important for Invoke_Scala;

--- a/src/Pure/System/isabelle_process.ML	Tue Jul 12 11:45:13 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:39:29 2011 +0200
@@ -66,17 +66,18 @@
 
 fun chunk s = [string_of_int (size s), "\n", s];
 
-fun message _ _ _ "" = ()
-  | message mbox ch raw_props body =
-      let
-        val robust_props = map (pairself YXML.escape_controls) raw_props;
-        val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
-      in Mailbox.send mbox (chunk header @ chunk body) end;
+fun message mbox ch raw_props body =
+  let
+    val robust_props = map (pairself YXML.escape_controls) raw_props;
+    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
+  in Mailbox.send mbox (chunk header @ chunk body) end;
 
 fun standard_message mbox with_serial ch body =
-  message mbox ch
-    ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
-      (Position.properties_of (Position.thread_data ()))) body;
+  if body = "" then ()
+  else
+    message mbox ch
+      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+        (Position.properties_of (Position.thread_data ()))) body;
 
 fun message_output mbox out_stream =
   let