moved message markup into Scala layer -- reduced redundancy;

--- a/src/Pure/General/markup.ML	Fri Jan 16 22:54:11 2009 +0100
+++ b/src/Pure/General/markup.ML	Fri Jan 16 22:56:12 2009 +0100
@@ -95,17 +95,7 @@
   val editN: string val edit: string -> string -> T
   val pidN: string
   val sessionN: string
-  val classN: string
-  val messageN: string val message: string -> T
   val promptN: string val prompt: T
-  val writelnN: string
-  val priorityN: string
-  val tracingN: string
-  val warningN: string
-  val errorN: string
-  val debugN: string
-  val initN: string
-  val statusN: string
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -284,19 +274,8 @@
 val pidN = "pid";
 val sessionN = "session";
 
-val classN = "class";
-val (messageN, message) = markup_string "message" classN;
-
 val (promptN, prompt) = markup_elem "prompt";
 
-val writelnN = "writeln";
-val priorityN = "priority";
-val tracingN = "tracing";
-val warningN = "warning";
-val errorN = "error";
-val debugN = "debug";
-val initN = "init";
-val statusN = "status";
 
 
 (* print mode operations *)

--- a/src/Pure/General/markup.scala	Fri Jan 16 22:54:11 2009 +0100
+++ b/src/Pure/General/markup.scala	Fri Jan 16 22:56:12 2009 +0100
@@ -131,6 +131,21 @@
   val SESSION = "session"
 
   val MESSAGE = "message"
+  val CLASS = "class"
+
+  val INIT = "init"
+  val STATUS = "status"
+  val WRITELN = "writeln"
+  val PRIORITY = "priority"
+  val TRACING = "tracing"
+  val WARNING = "warning"
+  val ERROR = "error"
+  val DEBUG = "debug"
+  val SYSTEM = "system"
+  val STDIN = "stdin"
+  val STDOUT = "stdout"
+  val SIGNAL = "signal"
+  val EXIT = "exit"
 
 
   /* content */

--- a/src/Pure/Tools/isabelle_process.ML	Fri Jan 16 22:54:11 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Jan 16 22:56:12 2009 +0100
@@ -55,9 +55,6 @@
   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_text class body =
-  YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
-
 fun message_pos trees = trees |> get_first
   (fn XML.Elem (name, atts, ts) =>
         if name = Markup.positionN then SOME (Position.of_properties atts)
@@ -69,21 +66,21 @@
 
 in
 
-fun message _ _ _ "" = ()
-  | message out_stream ch class body =
+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 = message_text class body;
+        val txt = clean_string [Symbol.STX] body;
       in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
 
 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 = message_text Markup.initN (Session.welcome ());
+    val text = Session.welcome ();
   in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
 
 end;
@@ -116,13 +113,13 @@
     val _ = SimpleThread.fork false (auto_flush out_stream);
     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn   := message out_stream "B" Markup.statusN;
-    Output.writeln_fn  := message out_stream "C" Markup.writelnN;
-    Output.priority_fn := message out_stream "D" Markup.priorityN;
-    Output.tracing_fn  := message out_stream "E" Markup.tracingN;
-    Output.warning_fn  := message out_stream "F" Markup.warningN;
-    Output.error_fn    := message out_stream "G" Markup.errorN;
-    Output.debug_fn    := message out_stream "H" Markup.debugN;
+    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.prompt_fn   := ignore;
     out_stream
   end;

--- a/src/Pure/Tools/isabelle_process.scala	Fri Jan 16 22:54:11 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Fri Jan 16 22:56:12 2009 +0100
@@ -50,6 +50,21 @@
       ('2' : Int) -> Kind.STDOUT,
       ('3' : Int) -> Kind.SIGNAL,
       ('4' : Int) -> Kind.EXIT)
+    // message markup
+    val markup = Map(
+      Kind.INIT -> Markup.INIT,
+      Kind.STATUS -> Markup.STATUS,
+      Kind.WRITELN -> Markup.WRITELN,
+      Kind.PRIORITY -> Markup.PRIORITY,
+      Kind.TRACING -> Markup.TRACING,
+      Kind.WARNING -> Markup.WARNING,
+      Kind.ERROR -> Markup.ERROR,
+      Kind.DEBUG -> Markup.DEBUG,
+      Kind.SYSTEM -> Markup.SYSTEM,
+      Kind.STDIN -> Markup.STDIN,
+      Kind.STDOUT -> Markup.STDOUT,
+      Kind.SIGNAL -> Markup.SIGNAL,
+      Kind.EXIT -> Markup.EXIT)
     //}}}
     def is_raw(kind: Value) =
       kind == STDOUT
@@ -67,8 +82,10 @@
 
   class Result(val kind: Kind.Value, val props: Properties, val result: String) {
     override def toString = {
-      val tree = YXML.parse_failsafe(result)
-      val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
+      val trees = YXML.parse_body_failsafe(result)
+      val res =
+        if (kind == Kind.STATUS) trees.map(_.toString).mkString
+        else trees.flatMap(XML.content(_).mkString).mkString
       if (props == null) kind.toString + " [[" + res + "]]"
       else kind.toString + " " + props.toString + " [[" + res + "]]"
     }
@@ -77,6 +94,10 @@
     def is_system = Kind.is_system(kind)
   }
 
+  def parse_message(kind: Kind.Value, result: String) = {
+    XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))),
+      YXML.parse_body_failsafe(result))
+  }
 }