tuned

--- a/Admin/jenkins/build/ci_build_benchmark.scala	Sat Jul 02 20:22:25 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Mon Jul 04 18:20:51 2016 +0200
@@ -14,4 +14,7 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
+  override def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
+    tree.selection()
+
 }

--- a/Admin/jenkins/build/ci_build_makeall.scala	Sat Jul 02 20:22:25 2016 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala	Mon Jul 04 18:20:51 2016 +0200
@@ -14,4 +14,7 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
+  override def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
+    tree.selection(all_sessions = true)
+
 }

--- a/src/Pure/Tools/ci_profile.scala	Sat Jul 02 20:22:25 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Mon Jul 04 18:20:51 2016 +0200
@@ -19,15 +19,11 @@
     println(name + "=" + Outer_Syntax.quote_string(value))
   }
 
-  protected def hg_id(path: Path): String =
-    Isabelle_System.hg("id -i", path.file).out
-
-  private def build(options: Options): (Build.Results, Time) =
+  private def build(options: Options): Build.Results =
   {
-    val start_time = Time.now()
     val progress = new Console_Progress(true)
-    val results = progress.interrupt_handler {
-      Build.build(
+    progress.interrupt_handler {
+      Build.build_selection(
         options = options,
         progress = progress,
         clean_build = true,
@@ -35,14 +31,9 @@
         max_jobs = jobs,
         dirs = include,
         select_dirs = select,
-        session_groups = groups,
-        all_sessions = all,
-        exclude_session_groups = exclude,
-        system_mode = true
-      )
+        system_mode = true,
+        selection = select_sessions _)
     }
-    val end_time = Time.now()
-    (results, end_time - start_time)
   }
 
   private def load_properties(): JProperties =
@@ -54,10 +45,27 @@
     props
   }
 
-  protected def print_section(title: String): Unit =
+  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
+  {
+    val timings = results.sessions.collect {
+      case session if group.forall(results.info(session).groups.contains(_)) =>
+        results(session).timing
+    }
+    (Timing.zero /: timings)(_ + _)
+  }
+
+
+  final def hg_id(path: Path): String =
+    Isabelle_System.hg("id -i", path.file).out
+
+  final def print_section(title: String): Unit =
     println(s"\n=== $title ===\n")
 
 
+  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
+  final val isabelle_id = hg_id(isabelle_home)
+
+
   override final def apply(args: List[String]): Unit =
   {
     print_section("CONFIGURATION")
@@ -65,8 +73,6 @@
     val props = load_properties()
     System.getProperties().putAll(props)
 
-    val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
-
     val options =
       Options.init()
         .bool.update("browser_info", true)
@@ -76,16 +82,17 @@
         .int.update("threads", threads)
 
     print_section("BUILD")
-    println(s"Build for Isabelle id ${hg_id(isabelle_home)}")
+    println(s"Build for Isabelle id $isabelle_id")
     pre_hook(args)
 
-    val (results, elapsed_time) = build(options)
+    val results = build(options)
 
     print_section("TIMING")
-    val total_timing =
-      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
-        copy(elapsed = elapsed_time)
-    println(total_timing.message_resources)
+
+    val groups = results.sessions.map(results.info).flatMap(_.groups)
+    for (group <- groups)
+      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
+    println("Overall: " + compute_timing(results, None).message_resources)
 
     if (!results.ok) {
       print_section("FAILED SESSIONS")
@@ -121,4 +128,13 @@
   def pre_hook(args: List[String]): Unit
   def post_hook(results: Build.Results): Unit
 
+  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
+    tree.selection(
+      requirements = false,
+      all_sessions = all,
+      exclude_session_groups = exclude,
+      exclude_sessions = Nil,
+      session_groups = groups,
+      sessions = Nil)
+
 }