# HG changeset patch
# User wenzelm
# Date 1475922847 -7200
# Node ID 1ec2adddf16b39b1631c25313b969ba713041344
# Parent  976289c733e6a1df9a1e03e88522ca575d19f7d9
prefer static Date_Format;

diff -r 976289c733e6 -r 1ec2adddf16b src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Sat Oct 08 12:20:20 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 12:34:07 2016 +0200
@@ -89,21 +89,6 @@
     }
 
     def apply(path: Path): Log_File = apply(path.file)
-  }
-
-  class Log_File private(val name: String, val lines: List[String])
-  {
-    log_file =>
-
-    override def toString: String = name
-
-    def text: String = cat_lines(lines)
-
-    def err(msg: String): Nothing =
-      error("Error in log file " + quote(name) + ": " + msg)
-
-
-    /* date format */
 
     val Date_Format =
     {
@@ -123,11 +108,26 @@
 
       Date.Format.make(fmts, tune)
     }
+  }
+
+  class Log_File private(val name: String, val lines: List[String])
+  {
+    log_file =>
+
+    override def toString: String = name
+
+    def text: String = cat_lines(lines)
+
+    def err(msg: String): Nothing =
+      error("Error in log file " + quote(name) + ": " + msg)
+
+
+    /* date format */
 
     object Strict_Date
     {
       def unapply(s: String): Some[Date] =
-        try { Some(Date_Format.parse(s)) }
+        try { Some(Log_File.Date_Format.parse(s)) }
         catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
     }