--- 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 */
--- 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_)
+ }
}