more flexible build_selection;

--- a/src/Pure/Tools/build.scala	Thu Jun 02 17:05:40 2016 +0200
+++ b/src/Pure/Tools/build.scala	Fri Jun 03 14:11:11 2016 +0200
@@ -434,31 +434,62 @@
   def build(
     options: Options,
     progress: Progress = Ignore_Progress,
-    requirements: Boolean = false,
-    all_sessions: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
-    exclude_session_groups: List[String] = Nil,
-    session_groups: List[String] = Nil,
     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,
+    requirements: Boolean = false,
+    all_sessions: Boolean = false,
+    exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
+    session_groups: List[String] = Nil,
     sessions: List[String] = Nil): Results =
   {
-    /* session tree and dependencies */
+    build_selection(
+      options = options,
+      progress = progress,
+      build_heap = build_heap,
+      clean_build = clean_build,
+      dirs = dirs,
+      select_dirs = select_dirs,
+      max_jobs = max_jobs,
+      list_files = list_files,
+      check_keywords = check_keywords,
+      no_build = no_build,
+      system_mode = system_mode,
+      verbose = verbose,
+      selection = { full_tree =>
+        full_tree.selection(requirements, all_sessions,
+          exclude_session_groups, exclude_sessions, session_groups, sessions) })
+  }
+
+  def build_selection(
+    options: Options,
+    progress: Progress = Ignore_Progress,
+    build_heap: Boolean = false,
+    clean_build: Boolean = false,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    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,
+    selection: Sessions.Tree => (List[String], Sessions.Tree) =
+      (_.selection(all_sessions = true))): Results =
+  {
+    /* session selection and dependencies */
 
     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
     val full_tree = Sessions.load(build_options, dirs, select_dirs)
-    val (selected, selected_tree) =
-      full_tree.selection(requirements, all_sessions,
-        exclude_session_groups, exclude_sessions, session_groups, sessions)
-
+    val (selected, selected_tree) = selection(full_tree)
     val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
 
     def session_sources_stamp(name: String): String =
@@ -784,9 +815,23 @@
     val start_time = Time.now()
     val results =
       progress.interrupt_handler {
-        build(options, progress, requirements, all_sessions, build_heap, clean_build,
-          dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
-          check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
+        build(options, progress,
+          build_heap = build_heap,
+          clean_build = clean_build,
+          dirs = dirs,
+          select_dirs = select_dirs,
+          max_jobs = max_jobs,
+          list_files = list_files,
+          check_keywords = check_keywords,
+          no_build = no_build,
+          system_mode = system_mode,
+          verbose = verbose,
+          requirements = requirements,
+          all_sessions = all_sessions,
+          exclude_session_groups = exclude_session_groups,
+          exclude_sessions = exclude_sessions,
+          session_groups = session_groups,
+          sessions = sessions)
       }
     val elapsed_time = Time.now() - start_time