equal
deleted
inserted
replaced
49 |
49 |
50 /** log file **/ |
50 /** log file **/ |
51 |
51 |
52 object Log_File |
52 object Log_File |
53 { |
53 { |
|
54 def apply(path: Path): Log_File = |
|
55 { |
|
56 val (path_name, ext) = path.expand.split_ext |
|
57 val text = |
|
58 if (ext == "gz") File.read_gzip(path) |
|
59 else if (ext == "xz") File.read_xz(path) |
|
60 else File.read(path) |
|
61 apply(path_name.base.implode, text) |
|
62 } |
|
63 |
54 def apply(name: String, lines: List[String]): Log_File = |
64 def apply(name: String, lines: List[String]): Log_File = |
55 new Log_File(name, lines) |
65 new Log_File(name, lines) |
56 |
66 |
57 def apply(name: String, text: String): Log_File = |
67 def apply(name: String, text: String): Log_File = |
58 Log_File(name, Library.trim_split_lines(text)) |
68 Log_File(name, Library.trim_split_lines(text)) |