# 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 " +