--- a/src/Pure/Admin/build_log.scala Tue Oct 31 16:24:07 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Tue Oct 31 16:45:39 2023 +0100
@@ -108,11 +108,11 @@
def apply(name: String, text: String): Log_File =
new Log_File(plain_name(name), Library.trim_split_lines(text))
- def read(file: JFile): Log_File = {
+ def read(file: JFile, cache: Compress.Cache = Compress.Cache.none): Log_File = {
val name = file.getName
val text =
if (File.is_gz(name)) File.read_gzip(file)
- else if (File.is_xz(name)) File.read_xz(file)
+ else if (File.is_xz(name)) Bytes.read(file).uncompress_xz(cache = cache).text
else File.read(file)
apply(name, text)
}
@@ -1084,7 +1084,7 @@
for (file <- files.iterator if status.exists(_.required(file))) {
val log_name = Log_File.plain_name(file)
progress.echo("Log " + quote(log_name), verbose = true)
- Exn.result { Log_File.read(file) } match {
+ Exn.result { Log_File.read(file, cache = cache.compress) } match {
case Exn.Res(log_file) => consumer.send(log_file)
case Exn.Exn(exn) => add_error(log_name, exn)
}