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))) } }