# HG changeset patch
# User wenzelm
# Date 1491563263 -7200
# Node ID b606c98e6d109a9fe18e0c3b0ffe7d2e44243426
# Parent  6389e3ec32ec8e44f98b153d6b92d7ad55a94f1a
tuned signature;

diff -r 6389e3ec32ec -r b606c98e6d10 src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Fri Apr 07 11:53:44 2017 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Fri Apr 07 13:07:43 2017 +0200
@@ -19,7 +19,7 @@
     val progress = new Console_Progress(verbose = true)
     val start_time = Time.now()
     val results = progress.interrupt_handler {
-      Build.build_selection(
+      Build.build(
         options = options,
         progress = progress,
         clean_build = clean,
diff -r 6389e3ec32ec -r b606c98e6d10 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 11:53:44 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 13:07:43 2017 +0200
@@ -185,7 +185,7 @@
 
   object Selection
   {
-    val all: Selection = Selection(all_sessions = true)
+    val empty: Selection = Selection()
   }
 
   sealed case class Selection(
@@ -196,6 +196,15 @@
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
+    def + (other: Selection): Selection =
+      Selection(
+        requirements = requirements || other.requirements,
+        all_sessions = all_sessions || other.all_sessions,
+        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
+        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
+        session_groups = session_groups ::: other.session_groups,
+        sessions = sessions ::: other.sessions)
+
     def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {
       val bad_sessions =
diff -r 6389e3ec32ec -r b606c98e6d10 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 07 11:53:44 2017 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 07 13:07:43 2017 +0200
@@ -351,50 +351,20 @@
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
-    sessions: List[String] = Nil): Results =
-  {
-    build_selection(
-      options = options,
-      progress = progress,
-      build_heap = build_heap,
-      clean_build = clean_build,
-      dirs = dirs,
-      select_dirs = select_dirs,
-      numa_shuffling = numa_shuffling,
-      max_jobs = max_jobs,
-      list_files = list_files,
-      check_keywords = check_keywords,
-      no_build = no_build,
-      system_mode = system_mode,
-      verbose = verbose,
-      pide = pide,
-      selection =
-        Sessions.Selection(requirements, all_sessions,
-          exclude_session_groups, exclude_sessions, session_groups, sessions))
-  }
-
-  def build_selection(
-      options: Options,
-      progress: Progress = No_Progress,
-      build_heap: Boolean = false,
-      clean_build: Boolean = false,
-      dirs: List[Path] = Nil,
-      select_dirs: List[Path] = Nil,
-      numa_shuffling: Boolean = false,
-      max_jobs: Int = 1,
-      list_files: Boolean = false,
-      check_keywords: Set[String] = Set.empty,
-      no_build: Boolean = false,
-      system_mode: Boolean = false,
-      verbose: Boolean = false,
-      pide: Boolean = false,
-      selection: Sessions.Selection = Sessions.Selection.all): Results =
+    sessions: List[String] = Nil,
+    selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
     /* session selection and dependencies */
 
     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+
     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
-    val (selected, selected_sessions) = full_sessions.selection(selection)
+
+    val (selected, selected_sessions) =
+      full_sessions.selection(
+          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+            exclude_sessions, session_groups, sessions) + selection)
+
     val deps =
       Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
         verbose = verbose, list_files = list_files, check_keywords = check_keywords,