5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
|
10 import java.io.{File => JFile} |
10 import java.time.ZonedDateTime |
11 import java.time.ZonedDateTime |
11 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
12 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
12 |
13 |
13 import scala.collection.mutable |
14 import scala.collection.mutable |
14 import scala.util.matching.Regex |
15 import scala.util.matching.Regex |
49 |
50 |
50 /** log file **/ |
51 /** log file **/ |
51 |
52 |
52 object Log_File |
53 object Log_File |
53 { |
54 { |
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 |
|
64 def apply(name: String, lines: List[String]): Log_File = |
55 def apply(name: String, lines: List[String]): Log_File = |
65 new Log_File(name, lines) |
56 new Log_File(name, lines) |
66 |
57 |
67 def apply(name: String, text: String): Log_File = |
58 def apply(name: String, text: String): Log_File = |
68 Log_File(name, Library.trim_split_lines(text)) |
59 Log_File(name, Library.trim_split_lines(text)) |
|
60 |
|
61 def apply(file: JFile): Log_File = |
|
62 { |
|
63 val name = file.getName |
|
64 val (base_name, text) = |
|
65 Library.try_unsuffix(".gz", name) match { |
|
66 case Some(base_name) => (base_name, File.read_gzip(file)) |
|
67 case None => |
|
68 Library.try_unsuffix(".xz", name) match { |
|
69 case Some(base_name) => (base_name, File.read_xz(file)) |
|
70 case None => (name, File.read(file)) |
|
71 } |
|
72 } |
|
73 apply(base_name, text) |
|
74 } |
|
75 |
|
76 def apply(path: Path): Log_File = apply(path.file) |
69 } |
77 } |
70 |
78 |
71 class Log_File private(val name: String, val lines: List[String]) |
79 class Log_File private(val name: String, val lines: List[String]) |
72 { |
80 { |
73 log_file => |
81 log_file => |