# HG changeset patch
# User wenzelm
# Date 1476557251 -7200
# Node ID 12aa3980f65c6d4ce1fe58d72cbcd8876f16d0ae
# Parent  b46969a851a94fbf381c7075cbaf923e24f6c39c
more operations;

diff -r b46969a851a9 -r 12aa3980f65c src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Oct 15 19:08:32 2016 +0200
+++ b/src/Pure/General/bytes.scala	Sat Oct 15 20:47:31 2016 +0200
@@ -9,7 +9,7 @@
 
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
-  OutputStream, InputStream, FileInputStream}
+  OutputStream, InputStream, FileInputStream, FileOutputStream}
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
@@ -58,6 +58,19 @@
 
   def read(file: JFile): Bytes =
     using(new FileInputStream(file))(read_stream(_, file.length.toInt))
+
+  def read(path: Path): Bytes = read(path.file)
+
+
+  /* write */
+
+  def write(file: JFile, bytes: Bytes)
+  {
+    val stream = new FileOutputStream(file)
+    try { bytes.write_stream(stream) } finally { stream.close }
+  }
+
+  def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(