tuned error;
authorwenzelm
Sat Oct 08 11:21:29 2016 +0200 (2016-10-08)
changeset 641009b1573213ebe
parent 64099 7a273824e206
child 64101 976289c733e6
tuned error;
src/Pure/General/date.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Sat Oct 08 11:04:47 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 11:21:29 2016 +0200
     1.3 @@ -47,10 +47,6 @@
     1.4  
     1.5      def unapply(str: String): Option[Date] =
     1.6        try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
     1.7 -    object Strict
     1.8 -    {
     1.9 -      def unapply(s: String): Some[Date] = Some(parse(s))
    1.10 -    }
    1.11    }
    1.12  
    1.13    object Formatter
     2.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 11:04:47 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 11:21:29 2016 +0200
     2.3 @@ -7,8 +7,10 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +import java.time.ZoneId
     2.9 +import java.time.format.DateTimeParseException
    2.10  import java.util.Locale
    2.11 -import java.io.{File => JFile}
    2.12  
    2.13  import scala.collection.mutable
    2.14  import scala.util.matching.Regex
    2.15 @@ -47,6 +49,7 @@
    2.16    }
    2.17  
    2.18  
    2.19 +
    2.20    /** log file **/
    2.21  
    2.22    object Log_File
    2.23 @@ -200,13 +203,20 @@
    2.24  
    2.25    private def parse_header(log_file: Log_File): Header =
    2.26    {
    2.27 +    object Strict_Date
    2.28 +    {
    2.29 +      def unapply(s: String): Some[Date] =
    2.30 +        try { Some(Date_Format.parse(s)) }
    2.31 +        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
    2.32 +    }
    2.33 +
    2.34      def parse(kind: Kind.Value, start: Date, hostname: String,
    2.35        Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
    2.36      {
    2.37        val start_date = Field.build_start -> start.toString
    2.38        val end_date =
    2.39          log_file.lines.last match {
    2.40 -          case Test_End(Date_Format.Strict(end_date)) =>
    2.41 +          case Test_End(Strict_Date(end_date)) =>
    2.42              List(Field.build_end -> end_date.toString)
    2.43            case _ => Nil
    2.44          }
    2.45 @@ -226,15 +236,15 @@
    2.46      }
    2.47  
    2.48      log_file.lines match {
    2.49 -      case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
    2.50 +      case Isatest.Test_Start(Strict_Date(start), hostname) :: _ =>
    2.51          parse(Kind.ISATEST, start, hostname,
    2.52            Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    2.53  
    2.54 -      case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
    2.55 +      case AFP.Test_Start(Strict_Date(start), hostname) :: _ =>
    2.56          parse(Kind.AFP_TEST, start, hostname,
    2.57            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    2.58  
    2.59 -      case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
    2.60 +      case AFP.Test_Start_Old(Strict_Date(start)) :: _ =>
    2.61          parse(Kind.AFP_TEST, start, "",
    2.62            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    2.63