# HG changeset patch
# User wenzelm
# Date 1493382563 -7200
# Node ID c937984c70e9fa6de91cce8f33d1dd42e05edf28
# Parent  d2f83588080fe26814aef1471e7939913dc866c4
tuned signature;

diff -r d2f83588080f -r c937984c70e9 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 14:23:55 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 14:29:23 2017 +0200
@@ -97,23 +97,6 @@
     Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log"))
 
 
-  /* log file collections */
-
-  def is_log(file: JFile,
-    prefixes: Iterable[String] =
-      List(Build_History.log_prefix, Isatest.log_prefix, AFP_Test.log_prefix),
-    suffixes: Iterable[String] =
-      List(".log", ".log.gz", ".log.xz")): Boolean =
-  {
-    val name = file.getName
-    prefixes.iterator.exists(name.startsWith(_)) &&
-    suffixes.iterator.exists(name.endsWith(_))
-  }
-
-  def log_files(dirs: Iterable[Path]): List[JFile] =
-    dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
-
-
 
   /** log file **/
 
@@ -121,6 +104,8 @@
 
   object Log_File
   {
+    /* log file */
+
     def apply(name: String, lines: List[String]): Log_File =
       new Log_File(name, lines)
 
@@ -145,6 +130,23 @@
     def apply(path: Path): Log_File = apply(path.file)
 
 
+    /* log file collections */
+
+    val suffixes: List[String] = List(".log", ".log.gz", ".log.xz")
+
+    def is_log(file: JFile,
+      prefixes: List[String] =
+        List(Build_History.log_prefix, Isatest.log_prefix, AFP_Test.log_prefix)): Boolean =
+    {
+      val name = file.getName
+      prefixes.exists(name.startsWith(_)) &&
+      suffixes.exists(name.endsWith(_))
+    }
+
+    def find_files(dirs: Iterable[Path]): List[JFile] =
+      dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
+
+
     /* date format */
 
     val Date_Format =