clarified modules;
authorwenzelm
Tue Oct 11 20:54:42 2016 +0200 (2016-10-11)
changeset 64150b10f2ddd7679
parent 64149 1380bf90d986
child 64151 be9b3cffe058
clarified modules;
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_history.scala	Tue Oct 11 20:31:13 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_history.scala	Tue Oct 11 20:54:42 2016 +0200
     1.3 @@ -19,14 +19,6 @@
     1.4    val BUILD_HISTORY = "build_history"
     1.5    val META_INFO_MARKER = "\fmeta_info = "
     1.6  
     1.7 -  def log_date(date: Date): String =
     1.8 -    String.format(Locale.ROOT, "%s.%05d",
     1.9 -      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
    1.10 -      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
    1.11 -
    1.12 -  def log_name(date: Date, parts: String*): String =
    1.13 -    (BUILD_HISTORY :: log_date(date) :: parts.toList).mkString("", "_", ".log.gz")
    1.14 -
    1.15  
    1.16  
    1.17    /** other Isabelle environment **/
    1.18 @@ -261,8 +253,8 @@
    1.19        /* output log */
    1.20  
    1.21        val log_path =
    1.22 -        other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
    1.23 -          Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
    1.24 +        other_isabelle.log_dir +
    1.25 +          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
    1.26  
    1.27        val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
    1.28  
     2.1 --- a/src/Pure/Tools/build_log.scala	Tue Oct 11 20:31:13 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Tue Oct 11 20:54:42 2016 +0200
     2.3 @@ -20,6 +20,20 @@
     2.4  {
     2.5    /** directory content **/
     2.6  
     2.7 +  /* file names */
     2.8 +
     2.9 +  def log_date(date: Date): String =
    2.10 +    String.format(Locale.ROOT, "%s.%05d",
    2.11 +      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
    2.12 +      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
    2.13 +
    2.14 +  def log_path(engine: String, date: Date, more: String*): Path =
    2.15 +    Path.explode(date.rep.getYear.toString) +
    2.16 +      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
    2.17 +
    2.18 +
    2.19 +  /* log file collections */
    2.20 +
    2.21    def is_log(file: JFile): Boolean =
    2.22      List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
    2.23