src/Pure/Admin/build_status.scala

 
 
   /* 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
 
     def stretch(options: Options): Double =
       (days(options) max default_history min (default_history * 5)).toDouble / default_history

             Build_Log.Prop.afp_version,
             Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
             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,
             Build_Log.Data.timing_gc,
             Build_Log.Data.ml_timing_elapsed,

         {
           val res = stmt.execute_query()
           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 =
                 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
                   case Threads_Option(Value.Int(i)) => i

 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
             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)))
             }
           }
         })
       }