# HG changeset patch
# User wenzelm
# Date 1475490516 -7200
# Node ID b4ece7a3f2ca7df7b3bd08c4ba816fd424b602b4
# Parent  73af1d36aeff853166cd8fd8fc7aa739e0f3e576
clarified stream operations;
added XZ data compression;

diff -r 73af1d36aeff -r b4ece7a3f2ca src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Oct 03 12:24:22 2016 +0200
+++ b/src/Pure/General/bytes.scala	Mon Oct 03 12:28:36 2016 +0200
@@ -8,7 +8,10 @@
 package isabelle
 
 
-import java.io.{File => JFile, OutputStream, InputStream, FileInputStream}
+import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
+  OutputStream, InputStream, FileInputStream}
+
+import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 
 object Bytes
@@ -38,25 +41,23 @@
 
   /* read */
 
-  def read_stream(stream: InputStream, max_length: Int): Bytes =
-  {
-    val bytes = new Array[Byte](max_length)
-    var i = 0
-    var m = 0
+  def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE): Bytes =
+    if (limit == 0) empty
+    else {
+      val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) 1024 else limit)
+      val buf = new Array[Byte](1024)
+      var m = 0
 
-    try {
       do {
-        m = stream.read(bytes, i, max_length - i)
-        if (m != -1) i += m
-      } while (m != -1 && max_length > i)
+        m = stream.read(buf, 0, buf.size min (limit - out.size))
+        if (m != -1) out.write(buf, 0, m)
+      } while (m != -1 && limit > out.size)
+
+      new Bytes(out.toByteArray, 0, out.size)
     }
-    finally { stream.close }
-
-    new Bytes(bytes, 0, i)
-  }
 
   def read(file: JFile): Bytes =
-    read_stream(new FileInputStream(file), file.length.toInt)
+    using(new FileInputStream(file))(read_stream(_, file.length.toInt))
 }
 
 final class Bytes private(
@@ -123,8 +124,21 @@
   }
 
 
-  /* write */
+  /* streams */
+
+  def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
+
+  def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
+
+
+  /* XZ data compression */
 
-  def write(stream: OutputStream): Unit = stream.write(bytes, offset, length)
+  def uncompress(): Bytes = using(new XZInputStream(stream()))(Bytes.read_stream(_))
+
+  def compress(options: XZ.Options = XZ.options()): Bytes =
+  {
+    val result = new ByteArrayOutputStream(length)
+    using(new XZOutputStream(result, options))(write_stream(_))
+    new Bytes(result.toByteArray, 0, result.size)
+  }
 }
-
diff -r 73af1d36aeff -r b4ece7a3f2ca src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Mon Oct 03 12:24:22 2016 +0200
+++ b/src/Pure/General/xz.scala	Mon Oct 03 12:28:36 2016 +0200
@@ -14,9 +14,7 @@
 {
   type Options = LZMA2Options
 
-  def options(): Options = options_preset(3)
-
-  def options_preset(preset: Int): Options =
+  def options(preset: Int = 3): Options =
   {
     val opts = new LZMA2Options
     opts.setPreset(preset)
diff -r 73af1d36aeff -r b4ece7a3f2ca src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Oct 03 12:24:22 2016 +0200
+++ b/src/Pure/PIDE/prover.scala	Mon Oct 03 12:28:36 2016 +0200
@@ -204,8 +204,8 @@
             {
               case chunks =>
                 try {
-                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
-                  chunks.foreach(_.write(stream))
+                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
+                  chunks.foreach(_.write_stream(stream))
                   stream.flush
                   true
                 }