# HG changeset patch
# User wenzelm
# Date 1281971062 -7200
# Node ID ba9ea6b9b75c5d1f4e10dd266cee598c9f331d09
# Parent  796904799f4d2e37cfd0a03ce44d9f2df1c92240
simplified internal message format: dropped special Symbol.STX header;

diff -r 796904799f4d -r ba9ea6b9b75c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Aug 16 16:24:22 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Aug 16 17:04:22 2010 +0200
@@ -1,11 +1,8 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
-Isabelle process wrapper.
-
-General format of process output:
-  (1) message = "\002"  header chunk  body chunk
-  (2) chunk = size (ASCII digits)  \n  content (YXML)
+Isabelle process wrapper, based on private fifos for maximum
+robustness and performance.
 *)
 
 signature ISABELLE_PROCESS =
@@ -57,11 +54,11 @@
 fun chunk s = string_of_int (size s) ^ "\n" ^ s;
 
 fun message _ _ _ "" = ()
-  | message out_stream ch props body =
+  | message out_stream ch raw_props body =
       let
-        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.escape_controls) props), []));
-        val msg = Symbol.STX ^ chunk header ^ chunk body;
-      in TextIO.output (out_stream, msg) (*atomic output*) end;
+        val robust_props = map (pairself YXML.escape_controls) raw_props;
+        val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
+      in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
 
 in
 
diff -r 796904799f4d -r ba9ea6b9b75c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Aug 16 16:24:22 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Aug 16 17:04:22 2010 +0200
@@ -288,26 +288,14 @@
 
       do {
         try {
-          //{{{
-          c = stream.read
-          var non_sync = 0
-          while (c >= 0 && c != 2) {
-            non_sync += 1
-            c = stream.read
+          val header = read_chunk()
+          val body = read_chunk()
+          header match {
+            case List(XML.Elem(Markup(name, props), Nil))
+                if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
+              put_result(Kind.markup(name(0)), props, body)
+            case _ => throw new Protocol_Error("bad header: " + header.toString)
           }
-          if (non_sync > 0)
-            throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
-          if (c == 2) {
-            val header = read_chunk()
-            val body = read_chunk()
-            header match {
-              case List(XML.Elem(Markup(name, props), Nil))
-                  if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
-                put_result(Kind.markup(name(0)), props, body)
-              case _ => throw new Protocol_Error("bad header: " + header.toString)
-            }
-          }
-          //}}}
         }
         catch {
           case e: IOException =>