src/Pure/Tools/isabelle_process.ML

--- a/src/Pure/Tools/isabelle_process.ML	Fri Jan 02 23:01:37 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Jan 02 23:12:26 2009 +0100
@@ -1,15 +1,14 @@
 (*  Title:      Pure/Tools/isabelle_process.ML
-    ID:         $Id$
     Author:     Makarius
 
 Isabelle process wrapper -- interaction via external program.
 
 General format of process output:
 
-  (a) unmarked stdout/stderr, no line structure (output should be
+  (1) unmarked stdout/stderr, no line structure (output should be
   processed immediately as it arrives);
 
-  (b) properly marked-up messages, e.g. for writeln channel
+  (2) properly marked-up messages, e.g. for writeln channel
 
   "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
 
@@ -17,13 +16,14 @@
   each, and the remaining text is any number of lines (output is
   supposed to be processed in one piece);
 
-  (c) special init message holds "pid" and "session" property.
+  (3) special init message holds "pid" and "session" property;
+
+  (4) message content is encoded in YXML format.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val isabelle_processN: string
-  val xmlN: string
   val init: string -> unit
 end;
 
@@ -33,7 +33,6 @@
 (* print modes *)
 
 val isabelle_processN = "isabelle_process";
-val xmlN = "XML";
 
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
@@ -57,18 +56,15 @@
   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
 
 fun message_text class ts =
-  let
-    val doc = XML.Elem (Markup.messageN, [(Markup.classN, class)], ts);
-    val msg =
-      if print_mode_active xmlN then XML.header ^ XML.string_of doc
-      else YXML.string_of doc;
-  in clean_string [Symbol.STX] msg end;
+  XML.Elem (Markup.messageN, [(Markup.classN, class)], ts)
+  |> YXML.string_of
+  |> clean_string [Symbol.STX];
 
-fun message_pos ts = get_first get_pos ts
-and get_pos (elem as XML.Elem (name, atts, ts)) =
-      if name = Markup.positionN then SOME (Position.of_properties atts)
-      else message_pos ts
-  | get_pos _ = NONE;
+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 output out_stream s = NAMED_CRITICAL "IO" (fn () =>
   (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
@@ -78,12 +74,12 @@
 fun message _ _ _ "" = ()
   | message out_stream ch class body =
       let
-        val (txt, pos) =
-          let val ts = YXML.parse_body body
-          in (message_text class ts, the_default Position.none (message_pos ts)) end;
+        val trees = YXML.parse_body body;
+        val pos = the_default Position.none (message_pos trees);
         val props =
           Position.properties_of (Position.thread_data ())
           |> Position.default_properties pos;
+        val txt = message_text class trees;
       in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
 
 fun init_message out_stream =