src/Pure/Admin/build_log.scala
changeset 78868 78fcd5bf6b2a
parent 78867 b02f8fb6b1b6
child 78875 b7d355b2b176
equal deleted inserted replaced
78867:b02f8fb6b1b6 78868:78fcd5bf6b2a
   106       new Log_File(plain_name(name), lines.map(Library.trim_line))
   106       new Log_File(plain_name(name), lines.map(Library.trim_line))
   107 
   107 
   108     def apply(name: String, text: String): Log_File =
   108     def apply(name: String, text: String): Log_File =
   109       new Log_File(plain_name(name), Library.trim_split_lines(text))
   109       new Log_File(plain_name(name), Library.trim_split_lines(text))
   110 
   110 
   111     def read(file: JFile): Log_File = {
   111     def read(file: JFile, cache: Compress.Cache = Compress.Cache.none): Log_File = {
   112       val name = file.getName
   112       val name = file.getName
   113       val text =
   113       val text =
   114         if (File.is_gz(name)) File.read_gzip(file)
   114         if (File.is_gz(name)) File.read_gzip(file)
   115         else if (File.is_xz(name)) File.read_xz(file)
   115         else if (File.is_xz(name)) Bytes.read(file).uncompress_xz(cache = cache).text
   116         else File.read(file)
   116         else File.read(file)
   117       apply(name, text)
   117       apply(name, text)
   118     }
   118     }
   119 
   119 
   120 
   120 
  1082 
  1082 
  1083       try {
  1083       try {
  1084         for (file <- files.iterator if status.exists(_.required(file))) {
  1084         for (file <- files.iterator if status.exists(_.required(file))) {
  1085           val log_name = Log_File.plain_name(file)
  1085           val log_name = Log_File.plain_name(file)
  1086           progress.echo("Log " + quote(log_name), verbose = true)
  1086           progress.echo("Log " + quote(log_name), verbose = true)
  1087           Exn.result { Log_File.read(file) } match {
  1087           Exn.result { Log_File.read(file, cache = cache.compress) } match {
  1088             case Exn.Res(log_file) => consumer.send(log_file)
  1088             case Exn.Res(log_file) => consumer.send(log_file)
  1089             case Exn.Exn(exn) => add_error(log_name, exn)
  1089             case Exn.Exn(exn) => add_error(log_name, exn)
  1090           }
  1090           }
  1091         }
  1091         }
  1092       }
  1092       }