# HG changeset patch
# User wenzelm
# Date 1476212082 -7200
# Node ID b10f2ddd7679cbea9e7a28b3b0da22e0c68cf4be
# Parent  1380bf90d98693f7d8bae615728510489d0aadf7
clarified modules;

diff -r 1380bf90d986 -r b10f2ddd7679 src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Tue Oct 11 20:31:13 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Tue Oct 11 20:54:42 2016 +0200
@@ -19,14 +19,6 @@
   val BUILD_HISTORY = "build_history"
   val META_INFO_MARKER = "\fmeta_info = "
 
-  def log_date(date: Date): String =
-    String.format(Locale.ROOT, "%s.%05d",
-      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
-      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
-
-  def log_name(date: Date, parts: String*): String =
-    (BUILD_HISTORY :: log_date(date) :: parts.toList).mkString("", "_", ".log.gz")
-
 
 
   /** other Isabelle environment **/
@@ -261,8 +253,8 @@
       /* output log */
 
       val log_path =
-        other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
-          Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
+        other_isabelle.log_dir +
+          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
 
       val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
 
diff -r 1380bf90d986 -r b10f2ddd7679 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Tue Oct 11 20:31:13 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Tue Oct 11 20:54:42 2016 +0200
@@ -20,6 +20,20 @@
 {
   /** directory content **/
 
+  /* file names */
+
+  def log_date(date: Date): String =
+    String.format(Locale.ROOT, "%s.%05d",
+      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
+      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
+
+  def log_path(engine: String, date: Date, more: String*): Path =
+    Path.explode(date.rep.getYear.toString) +
+      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+
+
+  /* log file collections */
+
   def is_log(file: JFile): Boolean =
     List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))