# HG changeset patch # User wenzelm # Date 1494096693 -7200 # Node ID 5a3052b2095f9d24e8bb353d75e7f66e84ecc15f # Parent dead160070972ffc421954808cd61a40bd510fca tuned signature; diff -r dead16007097 -r 5a3052b2095f src/Pure/Admin/build_status.scala --- 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) { diff -r dead16007097 -r 5a3052b2095f src/Pure/Admin/isabelle_cronjob.scala --- 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) diff -r dead16007097 -r 5a3052b2095f src/Pure/Admin/jenkins.scala --- 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 " +