# HG changeset patch
# User wenzelm
# Date 1222277593 -7200
# Node ID 7b605b8b719675085f2f3d6062b03ef3e581475c
# Parent  d0db291f7194512d210074cc7f503698b5fc683f
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);

diff -r d0db291f7194 -r 7b605b8b7196 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Wed Sep 24 18:08:42 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Wed Sep 24 19:33:13 2008 +0200
@@ -91,7 +91,7 @@
     val pid = (Markup.pidN, string_of_pid (Posix.ProcEnv.getpid ()));
     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
     val text = message_text Markup.initN [XML.Text (Session.welcome ())];
-  in output out_stream (special "H" ^ message_props [pid, session] ^ text ^ special_end) end;
+  in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
 
 end;
 
@@ -123,14 +123,14 @@
     val _ = SimpleThread.fork false (auto_flush out_stream);
     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.writeln_fn  := message out_stream "A" Markup.writelnN;
-    Output.priority_fn := message out_stream "B" Markup.priorityN;
-    Output.tracing_fn  := message out_stream "C" Markup.tracingN;
-    Output.warning_fn  := message out_stream "D" Markup.warningN;
-    Output.error_fn    := message out_stream "E" Markup.errorN;
-    Output.debug_fn    := message out_stream "F" Markup.debugN;
-    Output.prompt_fn   := message out_stream "G" Markup.promptN;
-    Output.status_fn   := message out_stream "I" Markup.statusN;
+    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.prompt_fn   := message out_stream "I" Markup.promptN;
     out_stream
   end;