clarified signature;
authorwenzelm
Wed, 26 Apr 2017 15:55:40 +0200
changeset 65588 b0d8d97198b3
parent 65580 66351f79c295
child 65589 f70c617e9c26
clarified signature;
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_history.scala	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Wed Apr 26 15:55:40 2017 +0200
@@ -16,7 +16,8 @@
 {
   /* log files */
 
-  val BUILD_HISTORY = "build_history"
+  val engine = "build_history"
+  val log_prefix = engine + "-"
   val META_INFO_MARKER = "\fmeta_info = "
 
 
@@ -198,7 +199,7 @@
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
-          Build_Log.log_filename(BUILD_HISTORY, build_history_date,
+          Build_Log.log_filename(Build_History.engine, build_history_date,
             List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
       val build_info =
@@ -215,7 +216,7 @@
         List(
           Build_Log.Prop.build_group_id -> build_group_id,
           Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
-          Build_Log.Prop.build_engine -> BUILD_HISTORY,
+          Build_Log.Prop.build_engine -> Build_History.engine,
           Build_Log.Prop.build_host -> build_host,
           Build_Log.Prop.build_start -> Build_Log.print_date(build_start),
           Build_Log.Prop.build_end -> Build_Log.print_date(build_end),
--- a/src/Pure/Admin/build_log.scala	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Apr 26 15:55:40 2017 +0200
@@ -90,14 +90,19 @@
 
   /* log file collections */
 
-  def is_log(file: JFile): Boolean =
-    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
+  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 isatest_files(dir: Path): List[JFile] =
-    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
-
-  def afp_test_files(dir: Path): List[JFile] =
-    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
+  def log_files(dirs: Iterable[Path]): List[JFile] =
+    dirs.iterator.flatMap(dir => File.find_files(dir.file, is_log(_))).toList
 
 
 
@@ -277,6 +282,7 @@
 
   object Isatest
   {
+    val log_prefix = "isatest-makeall-"
     val engine = "isatest"
     val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
     val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
@@ -286,6 +292,7 @@
 
   object AFP_Test
   {
+    val log_prefix = "afp-test-devel-"
     val engine = "afp-test"
     val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
     val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")