# HG changeset patch
# User wenzelm
# Date 1475917178 -7200
# Node ID 099518e8af2c687b4329e8a2a3755df4aa58c322
# Parent  5edeb60a7ec5062c91608696536bbaed39a7b72d
misc tuning and clarification;

diff -r 5edeb60a7ec5 -r 099518e8af2c src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Oct 07 23:11:20 2016 +0200
+++ b/src/Pure/General/date.scala	Sat Oct 08 10:59:38 2016 +0200
@@ -19,57 +19,57 @@
 {
   /* 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], filter: String => String = s => s): Format =
+    def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
     {
       require(fmts.nonEmpty)
 
-      @tailrec def parse_first(
-        last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor =
-      {
-        fs match {
-          case Nil => throw last_exn.get
-          case f :: rest =>
-            try { ZonedDateTime.from(f.parse(str)) }
-            catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) }
-        }
-      }
       new Format {
         def apply(date: Date): String = fmts.head.format(date.rep)
         def parse(str: String): Date =
-          new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str))))
+          new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
       }
     }
 
-    def make_variants(patterns: List[String],
-      locales: List[Locale] = List(Locale.ROOT),
-      filter: String => String = s => s): Format =
-    {
-      val fmts =
-        patterns.flatMap(pat =>
-          {
-            val fmt = DateTimeFormatter.ofPattern(pat)
-            locales.map(fmt.withLocale(_))
-          })
-      make(fmts, filter)
-    }
+    def apply(pats: String*): Format =
+      make(pats.toList.map(Date.Formatter.pattern(_)))
 
-    def apply(patterns: String*): Format =
-      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
-
-    val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
-    val date: Format = apply("dd-MMM-uuuu")
-    val time: Format = apply("HH:mm:ss")
+    val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
+    val date: Format = Format("dd-MMM-uuuu")
+    val time: Format = Format("HH:mm:ss")
   }
 
   abstract class Format private
   {
     def apply(date: Date): String
     def parse(str: String): Date
+
     def unapply(str: String): Option[Date] =
-      try { Some(parse(str)) }
-      catch { case _: DateTimeParseException => None }
+      try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
     object Strict
     {
       def unapply(s: String): Some[Date] = Some(parse(s))
diff -r 5edeb60a7ec5 -r 099518e8af2c src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 23:11:20 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 10:59:38 2016 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/build_log.scala
     Author:     Makarius
 
-Build log parsing for historic versions, back to "build_history_base".
+Build log parsing for historic versions.
 */
 
 package isabelle
@@ -9,8 +9,6 @@
 
 import java.util.Locale
 import java.io.{File => JFile}
-import java.time.ZonedDateTime
-import java.time.format.{DateTimeFormatter, DateTimeParseException}
 
 import scala.collection.mutable
 import scala.util.matching.Regex
@@ -144,7 +142,8 @@
   }
 
 
-  /* session log: produced by "isabelle build" */
+
+  /** session info: produced by "isabelle build" **/
 
   sealed case class Session_Info(
     session_name: String,
@@ -180,18 +179,26 @@
   }
 
 
-  /* header and meta data */
+
+  /** meta data **/
 
   val Date_Format =
-    Date.Format.make_variants(
-      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
-      List(Locale.ENGLISH, Locale.GERMAN),
-      // workaround for jdk-8u102
-      s => Word.implode(Word.explode(s).map({
+  {
+    val fmts =
+      Date.Formatter.variants(
+        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
+    def tune(s: String): String =
+      Word.implode(Word.explode(s).map({
         case "CET" | "MET" => "GMT+1"
         case "CEST" | "MEST" => "GMT+2"
         case "EST" => "GMT+1"  // FIXME ??
-        case a => a })))
+        case a => a }))
+
+    Date.Format.make(fmts, tune)
+  }
 
   object Header_Kind extends Enumeration
   {
@@ -271,7 +278,8 @@
   }
 
 
-  /* build info: produced by isabelle build */
+
+  /** build info: produced by isabelle build **/
 
   object Session_Status extends Enumeration
   {