# HG changeset patch
# User wenzelm
# Date 1219525658 -7200
# Node ID 46d7057b8614b0da626dee7e741608be1c4d8c32
# Parent  85b5f024d94b017c062981c6e096d6a6bf87abcf
added messages and process information;

diff -r 85b5f024d94b -r 46d7057b8614 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Aug 23 23:07:36 2008 +0200
+++ b/src/Pure/General/markup.ML	Sat Aug 23 23:07:38 2008 +0200
@@ -82,7 +82,6 @@
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
-  val promptN: string val prompt: T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
@@ -92,6 +91,19 @@
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val disposedN: string val disposed: 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 default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -156,7 +168,6 @@
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
-
 val (locationN, location) = markup_elem "location";
 
 
@@ -241,7 +252,6 @@
 
 (* toplevel *)
 
-val (promptN, prompt) = markup_elem "prompt";
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
 val (sendbackN, sendback) = markup_elem "sendback";
@@ -257,6 +267,26 @@
 val (disposedN, disposed) = markup_elem "disposed";
 
 
+(* messages *)
+
+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 *)
 
 fun default_output (_: T) = ("", "");