--- 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)
+ }
}
-
--- 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
--- /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
+ }
+}
--- 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))
- }
-}
-
--- 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
}
--- 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
--- 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")