diff -r b02f8fb6b1b6 -r 78fcd5bf6b2a src/Pure/Admin/build_log.scala --- 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) }