some support for raw messages, which bypass standard Symbol/YXML decoding;
authorwenzelm
Mon Jul 11 11:13:33 2011 +0200 (2011-07-11)
changeset 43746a41f618c641d
parent 43745 562e35bc351e
child 43747 74a9e9c8d5e8
some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;
src/Pure/General/markup.scala
src/Pure/General/output.ML
src/Pure/General/yxml.scala
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/System/standard_system.scala
     1.1 --- a/src/Pure/General/markup.scala	Mon Jul 11 10:27:50 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Mon Jul 11 11:13:33 2011 +0200
     1.3 @@ -321,6 +321,7 @@
     1.4    val TRACING = "tracing"
     1.5    val WARNING = "warning"
     1.6    val ERROR = "error"
     1.7 +  val RAW = "raw"
     1.8    val SYSTEM = "system"
     1.9    val STDOUT = "stdout"
    1.10    val EXIT = "exit"
     2.1 --- a/src/Pure/General/output.ML	Mon Jul 11 10:27:50 2011 +0200
     2.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 11:13:33 2011 +0200
     2.3 @@ -35,12 +35,14 @@
     2.4      val prompt_fn: (output -> unit) Unsynchronized.ref
     2.5      val status_fn: (output -> unit) Unsynchronized.ref
     2.6      val report_fn: (output -> unit) Unsynchronized.ref
     2.7 +    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     2.8    end
     2.9    val urgent_message: string -> unit
    2.10    val error_msg: string -> unit
    2.11    val prompt: string -> unit
    2.12    val status: string -> unit
    2.13    val report: string -> unit
    2.14 +  val raw_message: Properties.T -> string -> unit
    2.15  end;
    2.16  
    2.17  structure Output: OUTPUT =
    2.18 @@ -92,8 +94,9 @@
    2.19    val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.20    val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    2.21    val prompt_fn = Unsynchronized.ref raw_stdout;
    2.22 -  val status_fn = Unsynchronized.ref (fn _: string => ());
    2.23 -  val report_fn = Unsynchronized.ref (fn _: string => ());
    2.24 +  val status_fn = Unsynchronized.ref (fn _: output => ());
    2.25 +  val report_fn = Unsynchronized.ref (fn _: output => ());
    2.26 +  val raw_message_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
    2.27  end;
    2.28  
    2.29  fun writeln s = ! Private_Hooks.writeln_fn (output s);
    2.30 @@ -104,6 +107,7 @@
    2.31  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    2.32  fun status s = ! Private_Hooks.status_fn (output s);
    2.33  fun report s = ! Private_Hooks.report_fn (output s);
    2.34 +fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
    2.35  
    2.36  fun legacy_feature s = warning ("Legacy feature! " ^ s);
    2.37  
     3.1 --- a/src/Pure/General/yxml.scala	Mon Jul 11 10:27:50 2011 +0200
     3.2 +++ b/src/Pure/General/yxml.scala	Mon Jul 11 11:13:33 2011 +0200
     3.3 @@ -41,28 +41,6 @@
     3.4    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
     3.5  
     3.6  
     3.7 -  /* decoding pseudo UTF-8 */
     3.8 -
     3.9 -  private class Decode_Chars(decode: String => String,
    3.10 -    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
    3.11 -  {
    3.12 -    def length: Int = end - start
    3.13 -    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    3.14 -    def subSequence(i: Int, j: Int): CharSequence =
    3.15 -      new Decode_Chars(decode, buffer, start + i, start + j)
    3.16 -
    3.17 -    // toString with adhoc decoding: abuse of CharSequence interface
    3.18 -    override def toString: String = decode(Standard_System.decode_permissive_utf8(this))
    3.19 -  }
    3.20 -
    3.21 -  def decode_chars(decode: String => String,
    3.22 -    buffer: Array[Byte], start: Int, end: Int): CharSequence =
    3.23 -  {
    3.24 -    require(0 <= start && start <= end && end <= buffer.length)
    3.25 -    new Decode_Chars(decode, buffer, start, end)
    3.26 -  }
    3.27 -
    3.28 -
    3.29    /* parsing */
    3.30  
    3.31    private def err(msg: String) = error("Malformed YXML: " + msg)
     4.1 --- a/src/Pure/ROOT.ML	Mon Jul 11 10:27:50 2011 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Jul 11 11:13:33 2011 +0200
     4.3 @@ -27,9 +27,9 @@
     4.4  if Multithreading.available then ()
     4.5  else use "Concurrent/synchronized_sequential.ML";
     4.6  
     4.7 +use "General/properties.ML";
     4.8  use "General/output.ML";
     4.9  use "General/timing.ML";
    4.10 -use "General/properties.ML";
    4.11  use "General/markup.ML";
    4.12  use "General/scan.ML";
    4.13  use "General/source.ML";
     5.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jul 11 10:27:50 2011 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jul 11 11:13:33 2011 +0200
     5.3 @@ -108,6 +108,7 @@
     5.4      Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
     5.5      Output.Private_Hooks.warning_fn := standard_message mbox true "F";
     5.6      Output.Private_Hooks.error_fn := standard_message mbox true "G";
     5.7 +    Output.Private_Hooks.raw_message_fn := message mbox "H";
     5.8      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     5.9      Output.Private_Hooks.prompt_fn := ignore;
    5.10      message mbox "A" [] (Session.welcome ());
     6.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 10:27:50 2011 +0200
     6.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 11:13:33 2011 +0200
     6.3 @@ -29,7 +29,8 @@
     6.4        ('D' : Int) -> Markup.WRITELN,
     6.5        ('E' : Int) -> Markup.TRACING,
     6.6        ('F' : Int) -> Markup.WARNING,
     6.7 -      ('G' : Int) -> Markup.ERROR)
     6.8 +      ('G' : Int) -> Markup.ERROR,
     6.9 +      ('H' : Int) -> Markup.RAW)
    6.10    }
    6.11  
    6.12    abstract class Message
    6.13 @@ -54,6 +55,7 @@
    6.14      def is_system = kind == Markup.SYSTEM
    6.15      def is_status = kind == Markup.STATUS
    6.16      def is_report = kind == Markup.REPORT
    6.17 +    def is_raw = kind == Markup.RAW
    6.18      def is_ready = Isar_Document.is_ready(message)
    6.19      def is_syslog = is_init || is_exit || is_system || is_ready
    6.20  
    6.21 @@ -95,9 +97,13 @@
    6.22    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    6.23    {
    6.24      if (kind == Markup.INIT) rm_fifos()
    6.25 -    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    6.26 -    xml_cache.cache_tree(msg)((message: XML.Tree) =>
    6.27 -      receiver ! new Result(message.asInstanceOf[XML.Elem]))
    6.28 +    if (kind == Markup.RAW)
    6.29 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    6.30 +    else {
    6.31 +      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    6.32 +      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    6.33 +        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    6.34 +    }
    6.35    }
    6.36  
    6.37    private def put_result(kind: String, text: String)
    6.38 @@ -324,7 +330,7 @@
    6.39        val default_buffer = new Array[Byte](65536)
    6.40        var c = -1
    6.41  
    6.42 -      def read_chunk(): XML.Body =
    6.43 +      def read_chunk(decode: Boolean): XML.Body =
    6.44        {
    6.45          //{{{
    6.46          // chunk size
    6.47 @@ -351,19 +357,24 @@
    6.48  
    6.49          if (i != n) throw new Protocol_Error("bad message chunk content")
    6.50  
    6.51 -        YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
    6.52 +        if (decode)
    6.53 +          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
    6.54 +        else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
    6.55          //}}}
    6.56        }
    6.57  
    6.58        do {
    6.59          try {
    6.60 -          val header = read_chunk()
    6.61 -          val body = read_chunk()
    6.62 +          val header = read_chunk(true)
    6.63            header match {
    6.64              case List(XML.Elem(Markup(name, props), Nil))
    6.65                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
    6.66 -              put_result(Kind.message_markup(name(0)), props, body)
    6.67 -            case _ => throw new Protocol_Error("bad header: " + header.toString)
    6.68 +              val kind = Kind.message_markup(name(0))
    6.69 +              val body = read_chunk(kind != Markup.RAW)
    6.70 +              put_result(kind, props, body)
    6.71 +            case _ =>
    6.72 +              read_chunk(false)
    6.73 +              throw new Protocol_Error("bad header: " + header.toString)
    6.74            }
    6.75          }
    6.76          catch {
     7.1 --- a/src/Pure/System/session.scala	Mon Jul 11 10:27:50 2011 +0200
     7.2 +++ b/src/Pure/System/session.scala	Mon Jul 11 11:13:33 2011 +0200
     7.3 @@ -289,6 +289,7 @@
     7.4                case _ => bad_result(result)
     7.5              }
     7.6            }
     7.7 +          else if (result.is_raw) { } // FIXME
     7.8            else bad_result(result)
     7.9          }
    7.10      }
     8.1 --- a/src/Pure/System/standard_system.scala	Mon Jul 11 10:27:50 2011 +0200
     8.2 +++ b/src/Pure/System/standard_system.scala	Mon Jul 11 11:13:33 2011 +0200
     8.3 @@ -79,6 +79,25 @@
     8.4      buf.toString
     8.5    }
     8.6  
     8.7 +  private class Decode_Chars(decode: String => String,
     8.8 +    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
     8.9 +  {
    8.10 +    def length: Int = end - start
    8.11 +    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
    8.12 +    def subSequence(i: Int, j: Int): CharSequence =
    8.13 +      new Decode_Chars(decode, buffer, start + i, start + j)
    8.14 +
    8.15 +    // toString with adhoc decoding: abuse of CharSequence interface
    8.16 +    override def toString: String = decode(decode_permissive_utf8(this))
    8.17 +  }
    8.18 +
    8.19 +  def decode_chars(decode: String => String,
    8.20 +    buffer: Array[Byte], start: Int, end: Int): CharSequence =
    8.21 +  {
    8.22 +    require(0 <= start && start <= end && end <= buffer.length)
    8.23 +    new Decode_Chars(decode, buffer, start, end)
    8.24 +  }
    8.25 +
    8.26  
    8.27    /* basic file operations */
    8.28