tuned signature;
authorwenzelm
Sat May 06 20:51:33 2017 +0200 (2017-05-06)
changeset 657475a3052b2095f
parent 65746 dead16007097
child 65748 1f4a80e80c88
tuned signature;
src/Pure/Admin/build_status.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/jenkins.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 06 20:00:29 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 06 20:51:33 2017 +0200
     1.3 @@ -36,8 +36,7 @@
     1.4    }
     1.5  
     1.6    val standard_profiles: List[Profile] =
     1.7 -    Jenkins.build_log_profiles :::
     1.8 -    Isabelle_Cronjob.remote_builds.flatten.toList.map(r => Profile(r.name, r.sql))
     1.9 +    Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
    1.10  
    1.11    sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
    1.12    {
     2.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat May 06 20:00:29 2017 +0200
     2.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat May 06 20:51:33 2017 +0200
     2.3 @@ -97,13 +97,17 @@
     2.4      args: String = "",
     2.5      detect: SQL.Source = "")
     2.6    {
     2.7 -    def sql: SQL.Source =
     2.8 -      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
     2.9 -      Build_Log.Prop.build_host + " = " + SQL.string(host) +
    2.10 -      (if (detect == "") "" else " AND " + SQL.enclose(detect))
    2.11 +    def profile: Build_Status.Profile =
    2.12 +    {
    2.13 +      val sql =
    2.14 +        Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
    2.15 +        Build_Log.Prop.build_host + " = " + SQL.string(host) +
    2.16 +        (if (detect == "") "" else " AND " + SQL.enclose(detect))
    2.17 +      Build_Status.Profile(name, sql)
    2.18 +    }
    2.19    }
    2.20  
    2.21 -  val remote_builds: List[List[Remote_Build]] =
    2.22 +  private val remote_builds: List[List[Remote_Build]] =
    2.23    {
    2.24      List(
    2.25        List(Remote_Build("polyml-test", "lxbroy8",
    2.26 @@ -183,6 +187,9 @@
    2.27  
    2.28    /* present build status */
    2.29  
    2.30 +  val build_status_profiles: List[Build_Status.Profile] =
    2.31 +    remote_builds.flatten.map(_.profile)
    2.32 +
    2.33    def build_status(options: Options)
    2.34    {
    2.35      Build_Status.present_data(Build_Status.read_data(options), target_dir = build_status_dir)
     3.1 --- a/src/Pure/Admin/jenkins.scala	Sat May 06 20:00:29 2017 +0200
     3.2 +++ b/src/Pure/Admin/jenkins.scala	Sat May 06 20:51:33 2017 +0200
     3.3 @@ -48,11 +48,11 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* build log profiles */
     3.8 +  /* build log status */
     3.9  
    3.10    val build_log_jobs = List("isabelle-nightly-benchmark")
    3.11  
    3.12 -  val build_log_profiles: List[Build_Status.Profile] =
    3.13 +  val build_status_profiles: List[Build_Status.Profile] =
    3.14      build_log_jobs.map(job_name =>
    3.15        Build_Status.Profile("jenkins_" + job_name,
    3.16          Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +