# HG changeset patch
# User wenzelm
# Date 1509553754 -3600
# Node ID 8947cf58cb866df95a28af7b6ed5f69e2a10737d
# Parent  58b166fd84474c6bd2fe91698419802273429133
tuned output;

diff -r 58b166fd8447 -r 8947cf58cb86 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Wed Nov 01 17:07:43 2017 +0100
+++ b/src/Pure/Admin/build_status.scala	Wed Nov 01 17:29:14 2017 +0100
@@ -22,7 +22,7 @@
   /* data profiles */
 
   sealed case class Profile(
-    description: String, history: Int = 0, afp: Boolean = false, sql: String)
+    description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String)
   {
     def days(options: Options): Int = options.int("build_log_history") max history
 
@@ -168,6 +168,7 @@
             Build_Log.Settings.ML_PLATFORM,
             Build_Log.Data.session_name,
             Build_Log.Data.chapter,
+            Build_Log.Data.groups,
             Build_Log.Data.threads,
             Build_Log.Data.timing_elapsed,
             Build_Log.Data.timing_cpu,
@@ -191,6 +192,7 @@
           while (res.next()) {
             val session_name = res.string(Build_Log.Data.session_name)
             val chapter = res.string(Build_Log.Data.chapter)
+            val groups = split_lines(res.string(Build_Log.Data.groups))
             val threads =
             {
               val threads1 =
@@ -248,7 +250,7 @@
             val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
             val session = Session(session_name, threads, entry :: entries, ml_stats)
 
-            if (!afp || chapter == "AFP") {
+            if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))
             }
           }
diff -r 58b166fd8447 -r 8947cf58cb86 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 01 17:07:43 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 01 17:29:14 2017 +0100
@@ -123,6 +123,7 @@
     options: String = "",
     args: String = "",
     afp: Boolean = false,
+    slow: Boolean = false,
     detect: SQL.Source = "")
   {
     def sql: SQL.Source =
@@ -131,7 +132,7 @@
       (if (detect == "") "" else " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
-      Build_Status.Profile(description, history = history, afp = afp, sql = sql)
+      Build_Status.Profile(description, history = history, afp = afp, slow = slow, sql = sql)
 
     def pick(
       options: Options,
@@ -261,6 +262,7 @@
           options = "-m64 -M6 -U30000 -s10 -t AFP",
           args = "-g slow",
           afp = true,
+          slow = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
 
   private def remote_build_history(