# HG changeset patch
# User wenzelm
# Date 1475484567 -7200
# Node ID 7ecb22be8f03e338c2dbd36356ec408936d3b849
# Parent  445b3deced8f72d8529e8b2ba5b8772f78673959
more general read_stream: return actual byte count;

diff -r 445b3deced8f -r 7ecb22be8f03 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Oct 02 22:05:40 2016 +0200
+++ b/src/Pure/General/bytes.scala	Mon Oct 03 10:49:27 2016 +0200
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import java.io.{File => JFile, OutputStream, FileInputStream}
+import java.io.{File => JFile, OutputStream, InputStream, FileInputStream}
 
 
 object Bytes
@@ -38,24 +38,25 @@
 
   /* read */
 
-  def read(file: JFile): Bytes =
+  def read_stream(stream: InputStream, max_length: Int): Bytes =
   {
+    val bytes = new Array[Byte](max_length)
     var i = 0
     var m = 0
-    val n = file.length.toInt
-    val bytes = new Array[Byte](n)
 
-    val stream = new FileInputStream(file)
     try {
       do {
-        m = stream.read(bytes, i, n - i)
+        m = stream.read(bytes, i, max_length - i)
         if (m != -1) i += m
-      } while (m != -1 && n > i)
+      } while (m != -1 && max_length > i)
     }
     finally { stream.close }
 
-    new Bytes(bytes, 0, bytes.length)
+    new Bytes(bytes, 0, i)
   }
+
+  def read(file: JFile): Bytes =
+    read_stream(new FileInputStream(file), file.length.toInt)
 }
 
 final class Bytes private(