prefer static Date_Format;
authorwenzelm
Sat Oct 08 12:34:07 2016 +0200 (2016-10-08)
changeset 641021ec2adddf16b
parent 64101 976289c733e6
child 64103 60d163f38056
prefer static Date_Format;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 12:20:20 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 12:34:07 2016 +0200
     1.3 @@ -89,21 +89,6 @@
     1.4      }
     1.5  
     1.6      def apply(path: Path): Log_File = apply(path.file)
     1.7 -  }
     1.8 -
     1.9 -  class Log_File private(val name: String, val lines: List[String])
    1.10 -  {
    1.11 -    log_file =>
    1.12 -
    1.13 -    override def toString: String = name
    1.14 -
    1.15 -    def text: String = cat_lines(lines)
    1.16 -
    1.17 -    def err(msg: String): Nothing =
    1.18 -      error("Error in log file " + quote(name) + ": " + msg)
    1.19 -
    1.20 -
    1.21 -    /* date format */
    1.22  
    1.23      val Date_Format =
    1.24      {
    1.25 @@ -123,11 +108,26 @@
    1.26  
    1.27        Date.Format.make(fmts, tune)
    1.28      }
    1.29 +  }
    1.30 +
    1.31 +  class Log_File private(val name: String, val lines: List[String])
    1.32 +  {
    1.33 +    log_file =>
    1.34 +
    1.35 +    override def toString: String = name
    1.36 +
    1.37 +    def text: String = cat_lines(lines)
    1.38 +
    1.39 +    def err(msg: String): Nothing =
    1.40 +      error("Error in log file " + quote(name) + ": " + msg)
    1.41 +
    1.42 +
    1.43 +    /* date format */
    1.44  
    1.45      object Strict_Date
    1.46      {
    1.47        def unapply(s: String): Some[Date] =
    1.48 -        try { Some(Date_Format.parse(s)) }
    1.49 +        try { Some(Log_File.Date_Format.parse(s)) }
    1.50          catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
    1.51      }
    1.52