misc tuning and clarification;
authorwenzelm
Sat Oct 08 10:59:38 2016 +0200 (2016-10-08)
changeset 64098099518e8af2c
parent 64096 5edeb60a7ec5
child 64099 7a273824e206
misc tuning and clarification;
src/Pure/General/date.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Fri Oct 07 23:11:20 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 10:59:38 2016 +0200
     1.3 @@ -19,57 +19,57 @@
     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], filter: String => String = s => s): Format =
    1.33 +    def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
    1.34      {
    1.35        require(fmts.nonEmpty)
    1.36  
    1.37 -      @tailrec def parse_first(
    1.38 -        last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor =
    1.39 -      {
    1.40 -        fs match {
    1.41 -          case Nil => throw last_exn.get
    1.42 -          case f :: rest =>
    1.43 -            try { ZonedDateTime.from(f.parse(str)) }
    1.44 -            catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) }
    1.45 -        }
    1.46 -      }
    1.47        new Format {
    1.48          def apply(date: Date): String = fmts.head.format(date.rep)
    1.49          def parse(str: String): Date =
    1.50 -          new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str))))
    1.51 +          new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
    1.52        }
    1.53      }
    1.54  
    1.55 -    def make_variants(patterns: List[String],
    1.56 -      locales: List[Locale] = List(Locale.ROOT),
    1.57 -      filter: String => String = s => s): Format =
    1.58 -    {
    1.59 -      val fmts =
    1.60 -        patterns.flatMap(pat =>
    1.61 -          {
    1.62 -            val fmt = DateTimeFormatter.ofPattern(pat)
    1.63 -            locales.map(fmt.withLocale(_))
    1.64 -          })
    1.65 -      make(fmts, filter)
    1.66 -    }
    1.67 +    def apply(pats: String*): Format =
    1.68 +      make(pats.toList.map(Date.Formatter.pattern(_)))
    1.69  
    1.70 -    def apply(patterns: String*): Format =
    1.71 -      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
    1.72 -
    1.73 -    val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
    1.74 -    val date: Format = apply("dd-MMM-uuuu")
    1.75 -    val time: Format = apply("HH:mm:ss")
    1.76 +    val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
    1.77 +    val date: Format = Format("dd-MMM-uuuu")
    1.78 +    val time: Format = Format("HH:mm:ss")
    1.79    }
    1.80  
    1.81    abstract class Format private
    1.82    {
    1.83      def apply(date: Date): String
    1.84      def parse(str: String): Date
    1.85 +
    1.86      def unapply(str: String): Option[Date] =
    1.87 -      try { Some(parse(str)) }
    1.88 -      catch { case _: DateTimeParseException => None }
    1.89 +      try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
    1.90      object Strict
    1.91      {
    1.92        def unapply(s: String): Some[Date] = Some(parse(s))
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 23:11:20 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 10:59:38 2016 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Pure/Tools/build_log.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Build log parsing for historic versions, back to "build_history_base".
     2.8 +Build log parsing for historic versions.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12 @@ -9,8 +9,6 @@
    2.13  
    2.14  import java.util.Locale
    2.15  import java.io.{File => JFile}
    2.16 -import java.time.ZonedDateTime
    2.17 -import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.18  
    2.19  import scala.collection.mutable
    2.20  import scala.util.matching.Regex
    2.21 @@ -144,7 +142,8 @@
    2.22    }
    2.23  
    2.24  
    2.25 -  /* session log: produced by "isabelle build" */
    2.26 +
    2.27 +  /** session info: produced by "isabelle build" **/
    2.28  
    2.29    sealed case class Session_Info(
    2.30      session_name: String,
    2.31 @@ -180,18 +179,26 @@
    2.32    }
    2.33  
    2.34  
    2.35 -  /* header and meta data */
    2.36 +
    2.37 +  /** meta data **/
    2.38  
    2.39    val Date_Format =
    2.40 -    Date.Format.make_variants(
    2.41 -      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.42 -      List(Locale.ENGLISH, Locale.GERMAN),
    2.43 -      // workaround for jdk-8u102
    2.44 -      s => Word.implode(Word.explode(s).map({
    2.45 +  {
    2.46 +    val fmts =
    2.47 +      Date.Formatter.variants(
    2.48 +        List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.49 +        List(Locale.ENGLISH, Locale.GERMAN))
    2.50 +
    2.51 +    // workarounds undetected timezones
    2.52 +    def tune(s: String): String =
    2.53 +      Word.implode(Word.explode(s).map({
    2.54          case "CET" | "MET" => "GMT+1"
    2.55          case "CEST" | "MEST" => "GMT+2"
    2.56          case "EST" => "GMT+1"  // FIXME ??
    2.57 -        case a => a })))
    2.58 +        case a => a }))
    2.59 +
    2.60 +    Date.Format.make(fmts, tune)
    2.61 +  }
    2.62  
    2.63    object Header_Kind extends Enumeration
    2.64    {
    2.65 @@ -271,7 +278,8 @@
    2.66    }
    2.67  
    2.68  
    2.69 -  /* build info: produced by isabelle build */
    2.70 +
    2.71 +  /** build info: produced by isabelle build **/
    2.72  
    2.73    object Session_Status extends Enumeration
    2.74    {