src/Pure/Tools/build.scala
changeset 65419 457e4fbed731
parent 65415 8cd54b18b68b
child 65420 695d4e22345a
     1.1 --- a/src/Pure/Tools/build.scala	Thu Apr 06 21:37:13 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 10:47:25 2017 +0200
     1.3 @@ -368,9 +368,9 @@
     1.4        system_mode = system_mode,
     1.5        verbose = verbose,
     1.6        pide = pide,
     1.7 -      selection = { full_sessions =>
     1.8 -        full_sessions.selection(requirements, all_sessions,
     1.9 -          exclude_session_groups, exclude_sessions, session_groups, sessions) })
    1.10 +      selection =
    1.11 +        Sessions.Selection(requirements, all_sessions,
    1.12 +          exclude_session_groups, exclude_sessions, session_groups, sessions))
    1.13    }
    1.14  
    1.15    def build_selection(
    1.16 @@ -388,14 +388,13 @@
    1.17        system_mode: Boolean = false,
    1.18        verbose: Boolean = false,
    1.19        pide: Boolean = false,
    1.20 -      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
    1.21 -    ): Results =
    1.22 +      selection: Sessions.Selection = Sessions.Selection.all): Results =
    1.23    {
    1.24      /* session selection and dependencies */
    1.25  
    1.26      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    1.27      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    1.28 -    val (selected, selected_sessions) = selection(full_sessions)
    1.29 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    1.30      val deps =
    1.31        Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    1.32          verbose = verbose, list_files = list_files, check_keywords = check_keywords,