tuned;
authorwenzelm
Sat Oct 08 11:04:47 2016 +0200 (2016-10-08)
changeset 640997a273824e206
parent 64098 099518e8af2c
child 64100 9b1573213ebe
tuned;
src/Pure/General/date.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Sat Oct 08 10:59:38 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 11:04:47 2016 +0200
     1.3 @@ -19,29 +19,6 @@
     1.4  {
     1.5    /* format */
     1.6  
     1.7 -  object Formatter
     1.8 -  {
     1.9 -    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
    1.10 -
    1.11 -    def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
    1.12 -      pats.flatMap(pat => {
    1.13 -        val fmt = pattern(pat)
    1.14 -        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
    1.15 -      })
    1.16 -
    1.17 -    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
    1.18 -      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
    1.19 -    {
    1.20 -      fmts match {
    1.21 -        case Nil =>
    1.22 -          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
    1.23 -        case fmt :: rest =>
    1.24 -          try { ZonedDateTime.from(fmt.parse(str)) }
    1.25 -          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
    1.26 -      }
    1.27 -    }
    1.28 -  }
    1.29 -
    1.30    object Format
    1.31    {
    1.32      def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
    1.33 @@ -76,6 +53,29 @@
    1.34      }
    1.35    }
    1.36  
    1.37 +  object Formatter
    1.38 +  {
    1.39 +    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
    1.40 +
    1.41 +    def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
    1.42 +      pats.flatMap(pat => {
    1.43 +        val fmt = pattern(pat)
    1.44 +        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
    1.45 +      })
    1.46 +
    1.47 +    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
    1.48 +      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
    1.49 +    {
    1.50 +      fmts match {
    1.51 +        case Nil =>
    1.52 +          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
    1.53 +        case fmt :: rest =>
    1.54 +          try { ZonedDateTime.from(fmt.parse(str)) }
    1.55 +          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
    1.56 +      }
    1.57 +    }
    1.58 +  }
    1.59 +
    1.60  
    1.61    /* date operations */
    1.62  
     2.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 10:59:38 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 11:04:47 2016 +0200
     2.3 @@ -143,44 +143,25 @@
     2.4  
     2.5  
     2.6  
     2.7 -  /** session info: produced by "isabelle build" **/
     2.8 +  /** meta data **/
     2.9  
    2.10 -  sealed case class Session_Info(
    2.11 -    session_name: String,
    2.12 -    session_timing: Properties.T,
    2.13 -    command_timings: List[Properties.T],
    2.14 -    ml_statistics: List[Properties.T],
    2.15 -    task_statistics: List[Properties.T])
    2.16 -
    2.17 -  private def parse_session_info(
    2.18 -    log_file: Log_File,
    2.19 -    default_name: String,
    2.20 -    command_timings: Boolean,
    2.21 -    ml_statistics: Boolean,
    2.22 -    task_statistics: Boolean): Session_Info =
    2.23 +  object Field
    2.24    {
    2.25 -    val xml_cache = new XML.Cache()
    2.26 -
    2.27 -    val session_name =
    2.28 -      log_file.find_line("\fSession.name = ") match {
    2.29 -        case None => default_name
    2.30 -        case Some(name) if default_name == "" || default_name == name => name
    2.31 -        case Some(name) => log_file.err("log from different session " + quote(name))
    2.32 -      }
    2.33 -    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
    2.34 -    val command_timings_ =
    2.35 -      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
    2.36 -    val ml_statistics_ =
    2.37 -      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
    2.38 -    val task_statistics_ =
    2.39 -      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
    2.40 -
    2.41 -    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
    2.42 +    val build_host = "build_host"
    2.43 +    val build_start = "build_start"
    2.44 +    val build_end = "build_end"
    2.45 +    val isabelle_version = "isabelle_version"
    2.46 +    val afp_version = "afp_version"
    2.47    }
    2.48  
    2.49 -
    2.50 +  object Kind extends Enumeration
    2.51 +  {
    2.52 +    val ISATEST = Value("isatest")
    2.53 +    val AFP_TEST = Value("afp-test")
    2.54 +    val JENKINS = Value("jenkins")
    2.55 +  }
    2.56  
    2.57 -  /** meta data **/
    2.58 +  sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    2.59  
    2.60    val Date_Format =
    2.61    {
    2.62 @@ -189,7 +170,7 @@
    2.63          List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.64          List(Locale.ENGLISH, Locale.GERMAN))
    2.65  
    2.66 -    // workarounds undetected timezones
    2.67 +    // workaround undetected timezones
    2.68      def tune(s: String): String =
    2.69        Word.implode(Word.explode(s).map({
    2.70          case "CET" | "MET" => "GMT+1"
    2.71 @@ -200,25 +181,6 @@
    2.72      Date.Format.make(fmts, tune)
    2.73    }
    2.74  
    2.75 -  object Header_Kind extends Enumeration
    2.76 -  {
    2.77 -    val ISATEST = Value("isatest")
    2.78 -    val AFP_TEST = Value("afp-test")
    2.79 -    val JENKINS = Value("jenkins")
    2.80 -  }
    2.81 -
    2.82 -  sealed case class Header(
    2.83 -    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
    2.84 -
    2.85 -  object Field
    2.86 -  {
    2.87 -    val build_host = "build_host"
    2.88 -    val build_start = "build_start"
    2.89 -    val build_end = "build_end"
    2.90 -    val isabelle_version = "isabelle_version"
    2.91 -    val afp_version = "afp_version"
    2.92 -  }
    2.93 -
    2.94    object Isatest
    2.95    {
    2.96      val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
    2.97 @@ -238,7 +200,7 @@
    2.98  
    2.99    private def parse_header(log_file: Log_File): Header =
   2.100    {
   2.101 -    def parse(kind: Header_Kind.Value, start: Date, hostname: String,
   2.102 +    def parse(kind: Kind.Value, start: Date, hostname: String,
   2.103        Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
   2.104      {
   2.105        val start_date = Field.build_start -> start.toString
   2.106 @@ -265,14 +227,17 @@
   2.107  
   2.108      log_file.lines match {
   2.109        case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   2.110 -        parse(Header_Kind.ISATEST, start, hostname,
   2.111 +        parse(Kind.ISATEST, start, hostname,
   2.112            Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   2.113 +
   2.114        case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   2.115 -        parse(Header_Kind.AFP_TEST, start, hostname,
   2.116 +        parse(Kind.AFP_TEST, start, hostname,
   2.117            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   2.118 +
   2.119        case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
   2.120 -        parse(Header_Kind.AFP_TEST, start, "",
   2.121 +        parse(Kind.AFP_TEST, start, "",
   2.122            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   2.123 +
   2.124        case _ => log_file.err("cannot detect log header format")
   2.125      }
   2.126    }
   2.127 @@ -405,4 +370,41 @@
   2.128          }):_*)
   2.129      Build_Info(sessions)
   2.130    }
   2.131 +
   2.132 +
   2.133 +
   2.134 +  /** session info: produced by "isabelle build" **/
   2.135 +
   2.136 +  sealed case class Session_Info(
   2.137 +    session_name: String,
   2.138 +    session_timing: Properties.T,
   2.139 +    command_timings: List[Properties.T],
   2.140 +    ml_statistics: List[Properties.T],
   2.141 +    task_statistics: List[Properties.T])
   2.142 +
   2.143 +  private def parse_session_info(
   2.144 +    log_file: Log_File,
   2.145 +    default_name: String,
   2.146 +    command_timings: Boolean,
   2.147 +    ml_statistics: Boolean,
   2.148 +    task_statistics: Boolean): Session_Info =
   2.149 +  {
   2.150 +    val xml_cache = new XML.Cache()
   2.151 +
   2.152 +    val session_name =
   2.153 +      log_file.find_line("\fSession.name = ") match {
   2.154 +        case None => default_name
   2.155 +        case Some(name) if default_name == "" || default_name == name => name
   2.156 +        case Some(name) => log_file.err("log from different session " + quote(name))
   2.157 +      }
   2.158 +    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   2.159 +    val command_timings_ =
   2.160 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   2.161 +    val ml_statistics_ =
   2.162 +      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   2.163 +    val task_statistics_ =
   2.164 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   2.165 +
   2.166 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   2.167 +  }
   2.168  }