--- a/src/Pure/Admin/build_status.scala Sat May 06 20:00:29 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sat May 06 20:51:33 2017 +0200
@@ -36,8 +36,7 @@
}
val standard_profiles: List[Profile] =
- Jenkins.build_log_profiles :::
- Isabelle_Cronjob.remote_builds.flatten.toList.map(r => Profile(r.name, r.sql))
+ Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
{
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat May 06 20:00:29 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat May 06 20:51:33 2017 +0200
@@ -97,13 +97,17 @@
args: String = "",
detect: SQL.Source = "")
{
- def sql: SQL.Source =
- Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
- Build_Log.Prop.build_host + " = " + SQL.string(host) +
- (if (detect == "") "" else " AND " + SQL.enclose(detect))
+ def profile: Build_Status.Profile =
+ {
+ val sql =
+ Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
+ Build_Log.Prop.build_host + " = " + SQL.string(host) +
+ (if (detect == "") "" else " AND " + SQL.enclose(detect))
+ Build_Status.Profile(name, sql)
+ }
}
- val remote_builds: List[List[Remote_Build]] =
+ private val remote_builds: List[List[Remote_Build]] =
{
List(
List(Remote_Build("polyml-test", "lxbroy8",
@@ -183,6 +187,9 @@
/* present build status */
+ val build_status_profiles: List[Build_Status.Profile] =
+ remote_builds.flatten.map(_.profile)
+
def build_status(options: Options)
{
Build_Status.present_data(Build_Status.read_data(options), target_dir = build_status_dir)
--- a/src/Pure/Admin/jenkins.scala Sat May 06 20:00:29 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala Sat May 06 20:51:33 2017 +0200
@@ -48,11 +48,11 @@
}
- /* build log profiles */
+ /* build log status */
val build_log_jobs = List("isabelle-nightly-benchmark")
- val build_log_profiles: List[Build_Status.Profile] =
+ val build_status_profiles: List[Build_Status.Profile] =
build_log_jobs.map(job_name =>
Build_Status.Profile("jenkins_" + job_name,
Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +