src/Pure/System/isabelle_process.ML
changeset 52799 6a4498b048b7
parent 52787 c143ad7811fc
child 52800 1baa5d19ac44
     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 =