# HG changeset patch
# User wenzelm
# Date 1475438740 -7200
# Node ID 445b3deced8f72d8529e8b2ba5b8772f78673959
# Parent  5649a993666d9fcc3cec798fe324289109e5d5c6
clarified modules;

diff -r 5649a993666d -r 445b3deced8f src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Oct 02 21:05:14 2016 +0200
+++ b/src/Pure/General/file.scala	Sun Oct 02 22:05:40 2016 +0200
@@ -190,12 +190,14 @@
   }
 
   def read_stream(stream: InputStream): String =
-   read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
+    read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
 
   def read_gzip(file: JFile): String =
     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
+  def read_gzip(path: Path): String = read_gzip(path.file)
 
-  def read_gzip(path: Path): String = read_gzip(path.file)
+  def read_xz(file: JFile): String = read_stream(XZ.uncompress(new FileInputStream(file)))
+  def read_xz(path: Path): String = read_xz(path.file)
 
 
   /* read lines */
@@ -235,6 +237,11 @@
   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]): Unit = XZ.write_file(file, text)
+  def write_xz(file: JFile, text: CharSequence): Unit = XZ.write_file(file, List(text))
+  def write_xz(path: Path, text: Iterable[CharSequence]): Unit = XZ.write_file(path.file, text)
+  def write_xz(path: Path, text: CharSequence): Unit = XZ.write_file(path.file, List(text))
+
   def write_backup(path: Path, text: CharSequence)
   {
     path.file renameTo path.backup.file
diff -r 5649a993666d -r 445b3deced8f src/Pure/General/xz.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xz.scala	Sun Oct 02 22:05:40 2016 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Pure/General/xz.scala
+    Author:     Makarius
+
+XZ data compression.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream}
+
+import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
+
+
+object XZ
+{
+  def options(preset: Int): LZMA2Options =
+  {
+    val opts = new LZMA2Options
+    opts.setPreset(preset)
+    opts
+  }
+
+  def write_file(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
+  {
+    val opts = options(preset)
+    File.write_file(file, text,
+      (s: OutputStream) => new XZOutputStream(new BufferedOutputStream(s), opts))
+  }
+
+  def uncompress(s: InputStream): XZInputStream = new XZInputStream(new BufferedInputStream(s))
+}
diff -r 5649a993666d -r 445b3deced8f src/Pure/General/xz_file.scala
--- a/src/Pure/General/xz_file.scala	Sun Oct 02 21:05:14 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/*  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 5649a993666d -r 445b3deced8f src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Oct 02 21:05:14 2016 +0200
+++ b/src/Pure/build-jars	Sun Oct 02 22:05:40 2016 +0200
@@ -54,7 +54,7 @@
   General/url.scala
   General/value.scala
   General/word.scala
-  General/xz_file.scala
+  General/xz.scala
   Isar/document_structure.scala
   Isar/keyword.scala
   Isar/line_structure.scala