# HG changeset patch # User paulson # Date 1475500166 -3600 # Node ID 041cda506fb22860dd10263f930e204ea0188509 # Parent 0de4736dad8b37279f34cdca6094e9de9c8cba4c# Parent f6e965cf1617d3a92fdd2a6d9e4fc0e8450dca3a Merge diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Mon Oct 03 13:01:01 2016 +0100 +++ b/src/Pure/General/bytes.scala Mon Oct 03 14:09:26 2016 +0100 @@ -8,7 +8,10 @@ package isabelle -import java.io.{File => JFile, OutputStream, FileInputStream} +import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream, + OutputStream, InputStream, FileInputStream} + +import org.tukaani.xz.{XZInputStream, XZOutputStream} object Bytes @@ -38,24 +41,23 @@ /* read */ - def read(file: JFile): Bytes = - { - var i = 0 - var m = 0 - val n = file.length.toInt - val bytes = new Array[Byte](n) + def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes = + if (limit == 0) empty + else { + val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit) + val buf = new Array[Byte](8192) + var m = 0 - val stream = new FileInputStream(file) - try { do { - m = stream.read(bytes, i, n - i) - if (m != -1) i += m - } while (m != -1 && n > i) + m = stream.read(buf, 0, buf.size min (limit - out.size)) + if (m != -1) out.write(buf, 0, m) + } while (m != -1 && limit > out.size) + + new Bytes(out.toByteArray, 0, out.size) } - finally { stream.close } - new Bytes(bytes, 0, bytes.length) - } + def read(file: JFile): Bytes = + using(new FileInputStream(file))(read_stream(_, file.length.toInt)) } final class Bytes private( @@ -122,8 +124,22 @@ } - /* write */ + /* streams */ + + def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length) + + def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length) + + + /* XZ data compression */ - def write(stream: OutputStream): Unit = stream.write(bytes, offset, length) + def uncompress(): Bytes = + using(new XZInputStream(stream()))(Bytes.read_stream(_, hint = length)) + + def compress(options: XZ.Options = XZ.options()): Bytes = + { + val result = new ByteArrayOutputStream(length) + using(new XZOutputStream(result, options))(write_stream(_)) + new Bytes(result.toByteArray, 0, result.size) + } } - diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Mon Oct 03 13:01:01 2016 +0100 +++ b/src/Pure/General/file.scala Mon Oct 03 14:09:26 2016 +0100 @@ -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 @@ -190,12 +192,15 @@ } 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(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) + def read_xz(path: Path): String = read_xz(path.file) /* read lines */ @@ -215,26 +220,27 @@ /* 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: CharSequence, options: XZ.Options): Unit = + File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) + def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) + def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = + write_xz(path.file, text, options) + def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) + def write_backup(path: Path, text: CharSequence) { path.file renameTo path.backup.file diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/General/xz.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/xz.scala Mon Oct 03 14:09:26 2016 +0100 @@ -0,0 +1,23 @@ +/* Title: Pure/General/xz.scala + Author: Makarius + +Support for XZ data compression. +*/ + +package isabelle + + +import org.tukaani.xz.LZMA2Options + + +object XZ +{ + type Options = LZMA2Options + + def options(preset: Int = 3): Options = + { + val opts = new LZMA2Options + opts.setPreset(preset) + opts + } +} diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/General/xz_file.scala --- a/src/Pure/General/xz_file.scala Mon Oct 03 13:01:01 2016 +0100 +++ /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 0de4736dad8b -r 041cda506fb2 src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Mon Oct 03 13:01:01 2016 +0100 +++ b/src/Pure/PIDE/prover.scala Mon Oct 03 14:09:26 2016 +0100 @@ -204,8 +204,8 @@ { case chunks => try { - Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream) - chunks.foreach(_.write(stream)) + Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream) + chunks.foreach(_.write_stream(stream)) stream.flush true } diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/build-jars --- a/src/Pure/build-jars Mon Oct 03 13:01:01 2016 +0100 +++ b/src/Pure/build-jars Mon Oct 03 14:09:26 2016 +0100 @@ -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 diff -r 0de4736dad8b -r 041cda506fb2 src/Pure/library.scala --- a/src/Pure/library.scala Mon Oct 03 13:01:01 2016 +0100 +++ b/src/Pure/library.scala Mon Oct 03 14:09:26 2016 +0100 @@ -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")