tuned -- more uniform ML vs. Scala;

--- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 18:19:16 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 19:53:06 2013 +0200
@@ -155,12 +155,14 @@
     val n =
       (case Int.fromString len of
         SOME n => n
-      | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
+      | NONE => error ("Isabelle process: malformed header " ^ quote len));
     val chunk = System_Channel.inputN channel n;
-    val m = size chunk;
+    val i = size chunk;
   in
-    if m = n then chunk
-    else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
+    if i <> n then
+      error ("Isabelle process: bad chunk (unexpected EOF after " ^
+        string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
+    else chunk
   end;
 
 fun read_command channel =

--- a/src/Pure/System/isabelle_process.scala	Tue Jul 30 18:19:16 2013 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Jul 30 19:53:06 2013 +0200
@@ -289,10 +289,9 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(do_decode: Boolean): XML.Body =
+      def read_int(): Int =
+      //{{{
       {
-        //{{{
-        // chunk size
         var n = 0
         c = stream.read
         if (c == -1) throw new EOF
@@ -300,9 +299,16 @@
           n = 10 * n + (c - 48)
           c = stream.read
         }
-        if (c != 10) throw new Protocol_Error("bad message chunk header")
+        if (c != 10)
+          throw new Protocol_Error("malformed header: expected integer followed by newline")
+        else n
+      }
+      //}}}
 
-        // chunk content
+      def read_chunk(do_decode: Boolean): XML.Body =
+      //{{{
+      {
+        val n = read_int()
         val buf =
           if (n <= default_buffer.size) default_buffer
           else new Array[Byte](n)
@@ -312,20 +318,21 @@
         do {
           m = stream.read(buf, i, n - i)
           if (m != -1) i += m
-        } while (m != -1 && n > i)
+        }
+        while (m != -1 && n > i)
 
-        if (i != n) throw new Protocol_Error("bad message chunk content")
+        if (i != n)
+          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
 
         if (do_decode)
           YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
         else List(XML.Text(UTF8.decode_chars(s => s, buf, 0, n).toString))
-        //}}}
       }
+      //}}}
 
       try {
         do {
           try {
-            //{{{
             val header = read_chunk(true)
             header match {
               case List(XML.Elem(Markup(name, props), Nil)) =>
@@ -336,10 +343,10 @@
                 read_chunk(false)
                 throw new Protocol_Error("bad header: " + header.toString)
             }
-            //}}}
           }
           catch { case _: EOF => }
-        } while (c != -1)
+        }
+        while (c != -1)
       }
       catch {
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)