# HG changeset patch
# User wenzelm
# Date 1475484711 -7200
# Node ID 08f89f0e8a62772c2b1d344f38067b05fc6d724d
# Parent  7ecb22be8f03e338c2dbd36356ec408936d3b849
clarified modules;
afford explicit string composition in terminate_lines;

diff -r 7ecb22be8f03 -r 08f89f0e8a62 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Oct 03 10:49:27 2016 +0200
+++ b/src/Pure/General/file.scala	Mon Oct 03 10:51:51 2016 +0200
@@ -17,6 +17,8 @@
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
 
+import org.tukaani.xz.{XZInputStream, XZOutputStream}
+
 import scala.collection.mutable
 import scala.util.matching.Regex
 
@@ -196,7 +198,8 @@
     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(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(file: JFile): String =
+    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
   def read_xz(path: Path): String = read_xz(path.file)
 
 
@@ -217,30 +220,24 @@
 
   /* write */
 
-  def write_file(file: JFile, text: Iterable[CharSequence],
-    make_stream: OutputStream => OutputStream)
+  def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))
     val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))
-    try { text.iterator.foreach(writer.append(_)) }
-    finally { writer.close }
+    try { writer.append(text) } finally { writer.close }
   }
 
-  def write(file: JFile, text: Iterable[CharSequence]): Unit = write_file(file, text, (s) => s)
-  def write(file: JFile, text: CharSequence): Unit = write(file, List(text))
-  def write(path: Path, text: Iterable[CharSequence]): Unit = write(path.file, text)
+  def write(file: JFile, text: CharSequence): Unit = write_file(file, text, (s) => s)
   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
 
-  def write_gzip(file: JFile, text: Iterable[CharSequence]): Unit =
+  def write_gzip(file: JFile, text: CharSequence): Unit =
     write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
-  def write_gzip(file: JFile, text: CharSequence): Unit = write_gzip(file, List(text))
-  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_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
+    File.write_file(file, text, (s) => new XZOutputStream(new BufferedOutputStream(s), options))
+  def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
+    write_xz(path.file, text, options)
 
   def write_backup(path: Path, text: CharSequence)
   {
diff -r 7ecb22be8f03 -r 08f89f0e8a62 src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Mon Oct 03 10:49:27 2016 +0200
+++ b/src/Pure/General/xz.scala	Mon Oct 03 10:51:51 2016 +0200
@@ -1,32 +1,25 @@
 /*  Title:      Pure/General/xz.scala
     Author:     Makarius
 
-XZ data compression.
+Support for XZ data compression.
 */
 
 package isabelle
 
 
-import java.io.{File => JFile, BufferedOutputStream, OutputStream, InputStream, BufferedInputStream}
-
-import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
+import org.tukaani.xz.LZMA2Options
 
 
 object XZ
 {
-  def options(preset: Int): LZMA2Options =
+  type Options = LZMA2Options
+
+  def options(): Options = options_preset(3)
+
+  def options_preset(preset: Int): Options =
   {
     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 7ecb22be8f03 -r 08f89f0e8a62 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Oct 03 10:49:27 2016 +0200
+++ b/src/Pure/library.scala	Mon Oct 03 10:51:51 2016 +0200
@@ -99,11 +99,7 @@
 
   /* lines */
 
-  def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
-    new Iterable[CharSequence] {
-      def iterator: Iterator[CharSequence] =
-        lines.iterator.map(line => new Line_Termination(line))
-    }
+  def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
 
   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")