# HG changeset patch
# User wenzelm
# Date 1494429871 -7200
# Node ID d459db0f6135d02a601a5c4805fb48abac03709c
# Parent  d76c9c5c06564d1a6ac88447c7d6157bc441998d
actually plot extended profile history;

diff -r d76c9c5c0656 -r d459db0f6135 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Wed May 10 11:13:18 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Wed May 10 17:24:31 2017 +0200
@@ -11,7 +11,7 @@
 {
   /* data profiles */
 
-  sealed case class Profile(description: String, sql: String)
+  sealed case class Profile(description: String, history: Int, sql: String)
   {
     def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
     {
@@ -23,7 +23,7 @@
 
       Build_Log.Data.universal_table.select(columns, distinct = true,
         sql = "WHERE " +
-          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
+          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days max history) + " AND " +
           Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
           " AND " + sql_sessions + SQL.enclose(sql) +
           " ORDER BY " + Build_Log.Data.pull_date + " DESC")
diff -r d76c9c5c0656 -r d459db0f6135 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed May 10 11:13:18 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed May 10 17:24:31 2017 +0200
@@ -95,7 +95,7 @@
       (if (detect == "") "" else " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
-      Build_Status.Profile(description, sql)
+      Build_Status.Profile(description, history, sql)
 
     def pick(options: Options, rev: String = ""): Option[String] =
     {
diff -r d76c9c5c0656 -r d459db0f6135 src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Wed May 10 11:13:18 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Wed May 10 17:24:31 2017 +0200
@@ -54,7 +54,7 @@
 
   val build_status_profiles: List[Build_Status.Profile] =
     build_log_jobs.map(job_name =>
-      Build_Status.Profile("jenkins " + job_name,
+      Build_Status.Profile("jenkins " + job_name, 0,
         Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
         Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
         Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))