--- 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 ([^,]+)$""")