# HG changeset patch
# User wenzelm
# Date 1310375613 -7200
# Node ID a41f618c641d531bd797e0d9d07875b7b486fa9f
# Parent  562e35bc351eef52294e66de537bf412bf735d96
some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;

diff -r 562e35bc351e -r a41f618c641d src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/General/markup.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -321,6 +321,7 @@
   val TRACING = "tracing"
   val WARNING = "warning"
   val ERROR = "error"
+  val RAW = "raw"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val EXIT = "exit"
diff -r 562e35bc351e -r a41f618c641d src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 11 11:13:33 2011 +0200
@@ -35,12 +35,14 @@
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
+    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
+  val raw_message: Properties.T -> string -> unit
 end;
 
 structure Output: OUTPUT =
@@ -92,8 +94,9 @@
   val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
   val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
   val prompt_fn = Unsynchronized.ref raw_stdout;
-  val status_fn = Unsynchronized.ref (fn _: string => ());
-  val report_fn = Unsynchronized.ref (fn _: string => ());
+  val status_fn = Unsynchronized.ref (fn _: output => ());
+  val report_fn = Unsynchronized.ref (fn _: output => ());
+  val raw_message_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -104,6 +107,7 @@
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
+fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
 
 fun legacy_feature s = warning ("Legacy feature! " ^ s);
 
diff -r 562e35bc351e -r a41f618c641d src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/General/yxml.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -41,28 +41,6 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* decoding pseudo UTF-8 */
-
-  private class Decode_Chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
-  {
-    def length: Int = end - start
-    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
-    def subSequence(i: Int, j: Int): CharSequence =
-      new Decode_Chars(decode, buffer, start + i, start + j)
-
-    // toString with adhoc decoding: abuse of CharSequence interface
-    override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
-  }
-
-  def decode_chars(decode: String => String,
-    buffer: Array[Byte], start: Int, end: Int): CharSequence =
-  {
-    require(0 <= start && start <= end && end <= buffer.length)
-    new Decode_Chars(decode, buffer, start, end)
-  }
-
-
   /* parsing */
 
   private def err(msg: String) = error("Malformed YXML: " + msg)
diff -r 562e35bc351e -r a41f618c641d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 11 11:13:33 2011 +0200
@@ -27,9 +27,9 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
+use "General/properties.ML";
 use "General/output.ML";
 use "General/timing.ML";
-use "General/properties.ML";
 use "General/markup.ML";
 use "General/scan.ML";
 use "General/source.ML";
diff -r 562e35bc351e -r a41f618c641d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Jul 11 11:13:33 2011 +0200
@@ -108,6 +108,7 @@
     Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
     Output.Private_Hooks.warning_fn := standard_message mbox true "F";
     Output.Private_Hooks.error_fn := standard_message mbox true "G";
+    Output.Private_Hooks.raw_message_fn := message mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
     message mbox "A" [] (Session.welcome ());
diff -r 562e35bc351e -r a41f618c641d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -29,7 +29,8 @@
       ('D' : Int) -> Markup.WRITELN,
       ('E' : Int) -> Markup.TRACING,
       ('F' : Int) -> Markup.WARNING,
-      ('G' : Int) -> Markup.ERROR)
+      ('G' : Int) -> Markup.ERROR,
+      ('H' : Int) -> Markup.RAW)
   }
 
   abstract class Message
@@ -54,6 +55,7 @@
     def is_system = kind == Markup.SYSTEM
     def is_status = kind == Markup.STATUS
     def is_report = kind == Markup.REPORT
+    def is_raw = kind == Markup.RAW
     def is_ready = Isar_Document.is_ready(message)
     def is_syslog = is_init || is_exit || is_system || is_ready
 
@@ -95,9 +97,13 @@
   private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
     if (kind == Markup.INIT) rm_fifos()
-    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
-    xml_cache.cache_tree(msg)((message: XML.Tree) =>
-      receiver ! new Result(message.asInstanceOf[XML.Elem]))
+    if (kind == Markup.RAW)
+      receiver ! new Result(XML.Elem(Markup(kind, props), body))
+    else {
+      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
+      xml_cache.cache_tree(msg)((message: XML.Tree) =>
+        receiver ! new Result(message.asInstanceOf[XML.Elem]))
+    }
   }
 
   private def put_result(kind: String, text: String)
@@ -324,7 +330,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(): XML.Body =
+      def read_chunk(decode: Boolean): XML.Body =
       {
         //{{{
         // chunk size
@@ -351,19 +357,24 @@
 
         if (i != n) throw new Protocol_Error("bad message chunk content")
 
-        YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
+        if (decode)
+          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
+        else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
         //}}}
       }
 
       do {
         try {
-          val header = read_chunk()
-          val body = read_chunk()
+          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)) =>
-              put_result(Kind.message_markup(name(0)), props, body)
-            case _ => throw new Protocol_Error("bad header: " + header.toString)
+              val kind = Kind.message_markup(name(0))
+              val body = read_chunk(kind != Markup.RAW)
+              put_result(kind, props, body)
+            case _ =>
+              read_chunk(false)
+              throw new Protocol_Error("bad header: " + header.toString)
           }
         }
         catch {
diff -r 562e35bc351e -r a41f618c641d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -289,6 +289,7 @@
               case _ => bad_result(result)
             }
           }
+          else if (result.is_raw) { } // FIXME
           else bad_result(result)
         }
     }
diff -r 562e35bc351e -r a41f618c641d src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Jul 11 10:27:50 2011 +0200
+++ b/src/Pure/System/standard_system.scala	Mon Jul 11 11:13:33 2011 +0200
@@ -79,6 +79,25 @@
     buf.toString
   }
 
+  private class Decode_Chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
+  {
+    def length: Int = end - start
+    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    def subSequence(i: Int, j: Int): CharSequence =
+      new Decode_Chars(decode, buffer, start + i, start + j)
+
+    // toString with adhoc decoding: abuse of CharSequence interface
+    override def toString: String = decode(decode_permissive_utf8(this))
+  }
+
+  def decode_chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int): CharSequence =
+  {
+    require(0 <= start && start <= end && end <= buffer.length)
+    new Decode_Chars(decode, buffer, start, end)
+  }
+
 
   /* basic file operations */