# HG changeset patch
# User wenzelm
# Date 1285603893 -7200
# Node ID 5cb0d7b0d601c4ce0e8530da9c076c255e6471e7
# Parent  e4e1e3b69cbacd798686c98e9fef58f411c79930
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;

diff -r e4e1e3b69cba -r 5cb0d7b0d601 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Sep 27 18:10:21 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Sep 27 18:11:33 2010 +0200
@@ -335,8 +335,8 @@
         var m = 0
         do {
           m = stream.read(buf, i, n - i)
-          i += m
-        } while (m > 0 && n > i)
+          if (m != -1) i += m
+        } while (m != -1 && n > i)
 
         if (i != n) throw new Protocol_Error("bad message chunk content")