equal
deleted
inserted
replaced
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 } |