src/Pure/System/isabelle_process.ML
changeset 43771 fc524449f511
parent 43746 a41f618c641d
child 43772 c825594fd0c1
     1.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 12 11:45:13 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:39:29 2011 +0200
     1.3 @@ -66,17 +66,18 @@
     1.4  
     1.5  fun chunk s = [string_of_int (size s), "\n", s];
     1.6  
     1.7 -fun message _ _ _ "" = ()
     1.8 -  | message mbox ch raw_props body =
     1.9 -      let
    1.10 -        val robust_props = map (pairself YXML.escape_controls) raw_props;
    1.11 -        val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    1.12 -      in Mailbox.send mbox (chunk header @ chunk body) end;
    1.13 +fun message mbox ch raw_props body =
    1.14 +  let
    1.15 +    val robust_props = map (pairself YXML.escape_controls) raw_props;
    1.16 +    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    1.17 +  in Mailbox.send mbox (chunk header @ chunk body) end;
    1.18  
    1.19  fun standard_message mbox with_serial ch body =
    1.20 -  message mbox ch
    1.21 -    ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    1.22 -      (Position.properties_of (Position.thread_data ()))) body;
    1.23 +  if body = "" then ()
    1.24 +  else
    1.25 +    message mbox ch
    1.26 +      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    1.27 +        (Position.properties_of (Position.thread_data ()))) body;
    1.28  
    1.29  fun message_output mbox out_stream =
    1.30    let