1.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 18:19:16 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 19:53:06 2013 +0200
     1.3 @@ -155,12 +155,14 @@
     1.4      val n =
     1.5        (case Int.fromString len of
     1.6          SOME n => n
     1.7 -      | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
     1.8 +      | NONE => error ("Isabelle process: malformed header " ^ quote len));
     1.9      val chunk = System_Channel.inputN channel n;
    1.10 -    val m = size chunk;
    1.11 +    val i = size chunk;
    1.12    in
    1.13 -    if m = n then chunk
    1.14 -    else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
    1.15 +    if i <> n then
    1.16 +      error ("Isabelle process: bad chunk (unexpected EOF after " ^
    1.17 +        string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
    1.18 +    else chunk
    1.19    end;
    1.20  
    1.21  fun read_command channel =

     2.1 --- a/src/Pure/System/isabelle_process.scala	Tue Jul 30 18:19:16 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Jul 30 19:53:06 2013 +0200
     2.3 @@ -289,10 +289,9 @@
     2.4        val default_buffer = new Array[Byte](65536)
     2.5        var c = -1
     2.6  
     2.7 -      def read_chunk(do_decode: Boolean): XML.Body =
     2.8 +      def read_int(): Int =
     2.9 +      //{{{
    2.10        {
    2.11 -        //{{{
    2.12 -        // chunk size
    2.13          var n = 0
    2.14          c = stream.read
    2.15          if (c == -1) throw new EOF
    2.16 @@ -300,9 +299,16 @@
    2.17            n = 10 * n + (c - 48)
    2.18            c = stream.read
    2.19          }
    2.20 -        if (c != 10) throw new Protocol_Error("bad message chunk header")
    2.21 +        if (c != 10)
    2.22 +          throw new Protocol_Error("malformed header: expected integer followed by newline")
    2.23 +        else n
    2.24 +      }
    2.25 +      //}}}
    2.26  
    2.27 -        // chunk content
    2.28 +      def read_chunk(do_decode: Boolean): XML.Body =
    2.29 +      //{{{
    2.30 +      {
    2.31 +        val n = read_int()
    2.32          val buf =
    2.33            if (n <= default_buffer.size) default_buffer
    2.34            else new Array[Byte](n)
    2.35 @@ -312,20 +318,21 @@
    2.36          do {
    2.37            m = stream.read(buf, i, n - i)
    2.38            if (m != -1) i += m
    2.39 -        } while (m != -1 && n > i)
    2.40 +        }
    2.41 +        while (m != -1 && n > i)
    2.42  
    2.43 -        if (i != n) throw new Protocol_Error("bad message chunk content")
    2.44 +        if (i != n)
    2.45 +          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
    2.46  
    2.47          if (do_decode)
    2.48            YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
    2.49          else List(XML.Text(UTF8.decode_chars(s => s, buf, 0, n).toString))
    2.50 -        //}}}
    2.51        }
    2.52 +      //}}}
    2.53  
    2.54        try {
    2.55          do {
    2.56            try {
    2.57 -            //{{{
    2.58              val header = read_chunk(true)
    2.59              header match {
    2.60                case List(XML.Elem(Markup(name, props), Nil)) =>
    2.61 @@ -336,10 +343,10 @@
    2.62                  read_chunk(false)
    2.63                  throw new Protocol_Error("bad header: " + header.toString)
    2.64              }
    2.65 -            //}}}
    2.66            }
    2.67            catch { case _: EOF => }
    2.68 -        } while (c != -1)
    2.69 +        }
    2.70 +        while (c != -1)
    2.71        }
    2.72        catch {
    2.73          case e: IOException => system_output("Cannot read message:\n" + e.getMessage)