# HG changeset patch
# User wenzelm
# Date 1349115450 -7200
# Node ID c4e2762a265c38d8c41376476cd530269d4c6985
# Parent  882aa078eeae5cb784f3ba0c6d84df8869fb0919
more direct message header: eliminated historic encoding via single letter;

diff -r 882aa078eeae -r c4e2762a265c src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 20:16:37 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Mon Oct 01 20:17:30 2012 +0200
@@ -96,6 +96,13 @@
   val finishedN: string val finished: Markup.T
   val failedN: string val failed: Markup.T
   val serialN: string
+  val initN: string
+  val statusN: string
+  val writelnN: string
+  val tracingN: string
+  val warningN: string
+  val errorN: string
+  val protocolN: string
   val legacyN: string val legacy: Markup.T
   val promptN: string val prompt: Markup.T
   val reportN: string val report: Markup.T
@@ -291,6 +298,14 @@
 
 val serialN = "serial";
 
+val initN = "init";
+val statusN = "status";
+val writelnN = "writeln";
+val tracingN = "tracing";
+val warningN = "warning";
+val errorN = "error";
+val protocolN = "protocol";
+
 val (legacyN, legacy) = markup_elem "legacy";
 val (promptN, prompt) = markup_elem "prompt";
 
diff -r 882aa078eeae -r c4e2762a265c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:16:37 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Oct 01 20:17:30 2012 +0200
@@ -89,16 +89,16 @@
 
 fun chunk s = [string_of_int (size s), "\n", s];
 
-fun message do_flush mbox ch raw_props body =
+fun message do_flush mbox name raw_props body =
   let
     val robust_props = map (pairself YXML.embed_controls) raw_props;
-    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
+    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
   in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
 
-fun standard_message mbox opt_serial ch body =
+fun standard_message mbox opt_serial name body =
   if body = "" then ()
   else
-    message false mbox ch
+    message false mbox name
       ((case opt_serial of SOME i => cons (Isabelle_Markup.serialN, string_of_int i) | _ => I)
         (Position.properties_of (Position.thread_data ()))) body;
 
@@ -124,17 +124,22 @@
     val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
     val _ = Simple_Thread.fork false (message_output mbox channel);
   in
-    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
-    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
-    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
+    Output.Private_Hooks.status_fn := standard_message mbox NONE Isabelle_Markup.statusN;
+    Output.Private_Hooks.report_fn := standard_message mbox NONE Isabelle_Markup.reportN;
+    Output.Private_Hooks.writeln_fn :=
+      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.writelnN s);
     Output.Private_Hooks.tracing_fn :=
-      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
-    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
-    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
-    Output.Private_Hooks.protocol_message_fn := message true mbox "H";
+      (fn s =>
+        (update_tracing_limits s;
+          standard_message mbox (SOME (serial ())) Isabelle_Markup.tracingN s));
+    Output.Private_Hooks.warning_fn :=
+      (fn s => standard_message mbox (SOME (serial ())) Isabelle_Markup.warningN s);
+    Output.Private_Hooks.error_fn :=
+      (fn (i, s) => standard_message mbox (SOME i) Isabelle_Markup.errorN s);
+    Output.Private_Hooks.protocol_message_fn := message true mbox Isabelle_Markup.protocolN;
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
-    message true mbox "A" [] (Session.welcome ())
+    message true mbox Isabelle_Markup.initN [] (Session.welcome ())
   end;
 
 end;
diff -r 882aa078eeae -r c4e2762a265c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Oct 01 20:16:37 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Oct 01 20:17:30 2012 +0200
@@ -20,19 +20,6 @@
 {
   /* messages */
 
-  object Kind
-  {
-    val message_markup = Map(
-      ('A' : Int) -> Isabelle_Markup.INIT,
-      ('B' : Int) -> Isabelle_Markup.STATUS,
-      ('C' : Int) -> Isabelle_Markup.REPORT,
-      ('D' : Int) -> Isabelle_Markup.WRITELN,
-      ('E' : Int) -> Isabelle_Markup.TRACING,
-      ('F' : Int) -> Isabelle_Markup.WARNING,
-      ('G' : Int) -> Isabelle_Markup.ERROR,
-      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
-  }
-
   sealed abstract class Message
 
   class Input(name: String, args: List[String]) extends Message
@@ -375,9 +362,8 @@
             //{{{
             val header = read_chunk(true)
             header match {
-              case List(XML.Elem(Markup(name, props), Nil))
-                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
-                val kind = Kind.message_markup(name(0))
+              case List(XML.Elem(Markup(name, props), Nil)) =>
+                val kind = name.intern
                 val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
                 output_message(kind, props, body)
               case _ =>