# HG changeset patch
# User wenzelm
# Date 1373970668 -7200
# Node ID 9a360530eac8fc40856ad799c1571964db9b1850
# Parent  57a00f274130fface20ab4319476dab3ad37df9a
separate module XZ_File to avoid initial dependency on org.tukaani.xz;

diff -r 57a00f274130 -r 9a360530eac8 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jul 16 12:25:59 2013 +0200
+++ b/src/Pure/General/file.scala	Tue Jul 16 12:31:08 2013 +0200
@@ -14,8 +14,6 @@
 
 import scala.collection.mutable
 
-import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
-
 
 object File
 {
@@ -77,11 +75,6 @@
 
   def read_gzip(path: Path): String = read_gzip(path.file)
 
-  def read_xz(file: JFile): String =
-    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
-
-  def read_xz(path: Path): String = read_xz(path.file)
-
 
   /* read lines */
 
@@ -113,7 +106,7 @@
 
   /* write */
 
-  private def write_file(file: JFile, text: Iterable[CharSequence],
+  def write_file(file: JFile, text: Iterable[CharSequence],
     make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))
@@ -133,14 +126,6 @@
   def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)
   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
 
-  def write_xz(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
-  {
-    val options = new LZMA2Options
-    options.setPreset(preset)
-    write_file(file, text, (s: OutputStream) =>
-      new XZOutputStream(new BufferedOutputStream(s), options))
-  }
-
 
   /* copy */
 
diff -r 57a00f274130 -r 9a360530eac8 src/Pure/General/xz_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xz_file.scala	Tue Jul 16 12:31:08 2013 +0200
@@ -0,0 +1,31 @@
+/*  Title:      Pure/General/xz_file.scala
+    Author:     Makarius
+
+XZ file system operations.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedOutputStream, OutputStream, FileInputStream, BufferedInputStream,
+  File => JFile}
+
+import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
+
+
+object XZ_File
+{
+  def read(file: JFile): String =
+    File.read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
+
+  def read(path: Path): String = read(path.file)
+
+  def write(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
+  {
+    val options = new LZMA2Options
+    options.setPreset(preset)
+    File.write_file(file, text, (s: OutputStream) =>
+      new XZOutputStream(new BufferedOutputStream(s), options))
+  }
+}
+
diff -r 57a00f274130 -r 9a360530eac8 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jul 16 12:25:59 2013 +0200
+++ b/src/Pure/build-jars	Tue Jul 16 12:31:08 2013 +0200
@@ -27,6 +27,7 @@
   General/symbol.scala
   General/time.scala
   General/timing.scala
+  General/xz_file.scala
   Isar/keyword.scala
   Isar/outer_syntax.scala
   Isar/parse.scala