# HG changeset patch # User wenzelm # Date 1475917487 -7200 # Node ID 7a273824e206fa697c05afb62ec447fc6808dbbc # Parent 099518e8af2c687b4329e8a2a3755df4aa58c322 tuned; diff -r 099518e8af2c -r 7a273824e206 src/Pure/General/date.scala --- a/src/Pure/General/date.scala Sat Oct 08 10:59:38 2016 +0200 +++ b/src/Pure/General/date.scala Sat Oct 08 11:04:47 2016 +0200 @@ -19,29 +19,6 @@ { /* format */ - object Formatter - { - def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) - - def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] = - pats.flatMap(pat => { - val fmt = pattern(pat) - if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_)) - }) - - @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String, - last_exn: Option[DateTimeParseException] = None): TemporalAccessor = - { - fmts match { - case Nil => - throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0)) - case fmt :: rest => - try { ZonedDateTime.from(fmt.parse(str)) } - catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) } - } - } - } - object Format { def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = @@ -76,6 +53,29 @@ } } + object Formatter + { + def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) + + def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] = + pats.flatMap(pat => { + val fmt = pattern(pat) + if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_)) + }) + + @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String, + last_exn: Option[DateTimeParseException] = None): TemporalAccessor = + { + fmts match { + case Nil => + throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0)) + case fmt :: rest => + try { ZonedDateTime.from(fmt.parse(str)) } + catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) } + } + } + } + /* date operations */ diff -r 099518e8af2c -r 7a273824e206 src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Sat Oct 08 10:59:38 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Sat Oct 08 11:04:47 2016 +0200 @@ -143,44 +143,25 @@ - /** session info: produced by "isabelle build" **/ + /** meta data **/ - sealed case class Session_Info( - session_name: String, - session_timing: Properties.T, - command_timings: List[Properties.T], - ml_statistics: List[Properties.T], - task_statistics: List[Properties.T]) - - private def parse_session_info( - log_file: Log_File, - default_name: String, - command_timings: Boolean, - ml_statistics: Boolean, - task_statistics: Boolean): Session_Info = + object Field { - val xml_cache = new XML.Cache() - - val session_name = - log_file.find_line("\fSession.name = ") match { - case None => default_name - case Some(name) if default_name == "" || default_name == name => name - case Some(name) => log_file.err("log from different session " + quote(name)) - } - val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil - val command_timings_ = - if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil - val ml_statistics_ = - if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil - val task_statistics_ = - if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil - - Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) + val build_host = "build_host" + val build_start = "build_start" + val build_end = "build_end" + val isabelle_version = "isabelle_version" + val afp_version = "afp_version" } - + object Kind extends Enumeration + { + val ISATEST = Value("isatest") + val AFP_TEST = Value("afp-test") + val JENKINS = Value("jenkins") + } - /** meta data **/ + sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)]) val Date_Format = { @@ -189,7 +170,7 @@ List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), List(Locale.ENGLISH, Locale.GERMAN)) - // workarounds undetected timezones + // workaround undetected timezones def tune(s: String): String = Word.implode(Word.explode(s).map({ case "CET" | "MET" => "GMT+1" @@ -200,25 +181,6 @@ Date.Format.make(fmts, tune) } - object Header_Kind extends Enumeration - { - val ISATEST = Value("isatest") - val AFP_TEST = Value("afp-test") - val JENKINS = Value("jenkins") - } - - sealed case class Header( - kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)]) - - object Field - { - val build_host = "build_host" - val build_start = "build_start" - val build_end = "build_end" - val isabelle_version = "isabelle_version" - val afp_version = "afp_version" - } - object Isatest { val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""") @@ -238,7 +200,7 @@ private def parse_header(log_file: Log_File): Header = { - def parse(kind: Header_Kind.Value, start: Date, hostname: String, + def parse(kind: Kind.Value, start: Date, hostname: String, Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header = { val start_date = Field.build_start -> start.toString @@ -265,14 +227,17 @@ log_file.lines match { case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ => - parse(Header_Kind.ISATEST, start, hostname, + parse(Kind.ISATEST, start, hostname, Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version) + case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ => - parse(Header_Kind.AFP_TEST, start, hostname, + parse(Kind.AFP_TEST, start, hostname, AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version) + case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ => - parse(Header_Kind.AFP_TEST, start, "", + parse(Kind.AFP_TEST, start, "", AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version) + case _ => log_file.err("cannot detect log header format") } } @@ -405,4 +370,41 @@ }):_*) Build_Info(sessions) } + + + + /** session info: produced by "isabelle build" **/ + + sealed case class Session_Info( + session_name: String, + session_timing: Properties.T, + command_timings: List[Properties.T], + ml_statistics: List[Properties.T], + task_statistics: List[Properties.T]) + + private def parse_session_info( + log_file: Log_File, + default_name: String, + command_timings: Boolean, + ml_statistics: Boolean, + task_statistics: Boolean): Session_Info = + { + val xml_cache = new XML.Cache() + + val session_name = + log_file.find_line("\fSession.name = ") match { + case None => default_name + case Some(name) if default_name == "" || default_name == name => name + case Some(name) => log_file.err("log from different session " + quote(name)) + } + val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil + val command_timings_ = + if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil + val ml_statistics_ = + if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil + val task_statistics_ = + if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil + + Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) + } }