simplified message format: chunks with explicit size in bytes;
robust message header via YXML.binary_text;
standard_message: refer to thread position only;
discontinued obsolete "-" output stream;
tuned;

--- a/src/Pure/System/isabelle_process.ML	Thu Dec 17 13:58:15 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Dec 17 15:09:07 2009 +0100
@@ -1,24 +1,11 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
-Isabelle process wrapper -- interaction via external program.
+Isabelle process wrapper.
 
 General format of process output:
-
-  (1) unmarked stdout/stderr, no line structure (output should be
-  processed immediately as it arrives);
-
-  (2) properly marked-up messages, e.g. for writeln channel
-
-  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
-
-  where the props consist of name=value lines terminated by "\002,\n"
-  each, and the remaining text is any number of lines (output is
-  supposed to be processed in one piece);
-
-  (3) special init message holds "pid" and "session" property;
-
-  (4) message content is encoded in YXML format.
+  (1) message = "\002"  header chunk  body chunk
+  (2) chunk = size (ASCII digits)  \n  content (YXML)
 *)
 
 signature ISABELLE_PROCESS =
@@ -40,47 +27,28 @@
 
 (* message markup *)
 
-fun special ch = Symbol.STX ^ ch;
-val special_sep = special ",";
-val special_end = special ".";
-
 local
 
-fun clean_string bad str =
-  if exists_string (member (op =) bad) str then
-    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
-  else str;
+fun chunk s = string_of_int (size s) ^ "\n" ^ s;
 
-fun message_props props =
-  let val clean = clean_string [Symbol.STX, "\n", "\r"]
-  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
-
-fun message_pos trees = trees |> get_first
-  (fn XML.Elem (name, atts, ts) =>
-        if name = Markup.positionN then SOME (Position.of_properties atts)
-        else message_pos ts
-    | _ => NONE);
+fun message _ _ _ "" = ()
+  | message out_stream ch props body =
+      let
+        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
+        val msg = Symbol.STX ^ chunk header ^ chunk body;
+      in TextIO.output (out_stream, msg) (*atomic output*) end;
 
 in
 
-fun message _ _ "" = ()
-  | message out_stream ch body =
-      let
-        val pos = the_default Position.none (message_pos (YXML.parse_body body));
-        val props =
-          Position.properties_of (Position.thread_data ())
-          |> Position.default_properties pos;
-        val txt = clean_string [Symbol.STX] body;
-        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
-      in TextIO.output (out_stream, msg) end;
+fun standard_message out_stream ch body =
+  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
 
 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 ();
-    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
-  in TextIO.output (out_stream, msg) end;
+  in message out_stream "A" [pid, session] text end;
 
 end;
 
@@ -100,25 +68,20 @@
 
 fun setup_channels out =
   let
-    val out_stream =
-      if out = "-" then TextIO.stdOut
-      else
-        let
-          val path = File.platform_path (Path.explode out);
-          val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
-          val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
-          val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
-        in out_stream end;
+    val path = File.platform_path (Path.explode out);
+    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
+    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
     val _ = SimpleThread.fork false (auto_flush out_stream);
+    val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn   := message out_stream "B";
-    Output.writeln_fn  := message out_stream "C";
-    Output.priority_fn := message out_stream "D";
-    Output.tracing_fn  := message out_stream "E";
-    Output.warning_fn  := message out_stream "F";
-    Output.error_fn    := message out_stream "G";
-    Output.debug_fn    := message out_stream "H";
+    Output.status_fn   := standard_message out_stream "B";
+    Output.writeln_fn  := standard_message out_stream "C";
+    Output.priority_fn := standard_message out_stream "D";
+    Output.tracing_fn  := standard_message out_stream "E";
+    Output.warning_fn  := standard_message out_stream "F";
+    Output.error_fn    := standard_message out_stream "G";
+    Output.debug_fn    := standard_message out_stream "H";
     Output.prompt_fn   := ignore;
     out_stream
   end;