# 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")