src/Pure/Tools/build.scala
changeset 65422 b606c98e6d10
parent 65420 695d4e22345a
child 65431 4a3e6cda3b94
     1.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 11:53:44 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 13:07:43 2017 +0200
     1.3 @@ -351,50 +351,20 @@
     1.4      exclude_session_groups: List[String] = Nil,
     1.5      exclude_sessions: List[String] = Nil,
     1.6      session_groups: List[String] = Nil,
     1.7 -    sessions: List[String] = Nil): Results =
     1.8 -  {
     1.9 -    build_selection(
    1.10 -      options = options,
    1.11 -      progress = progress,
    1.12 -      build_heap = build_heap,
    1.13 -      clean_build = clean_build,
    1.14 -      dirs = dirs,
    1.15 -      select_dirs = select_dirs,
    1.16 -      numa_shuffling = numa_shuffling,
    1.17 -      max_jobs = max_jobs,
    1.18 -      list_files = list_files,
    1.19 -      check_keywords = check_keywords,
    1.20 -      no_build = no_build,
    1.21 -      system_mode = system_mode,
    1.22 -      verbose = verbose,
    1.23 -      pide = pide,
    1.24 -      selection =
    1.25 -        Sessions.Selection(requirements, all_sessions,
    1.26 -          exclude_session_groups, exclude_sessions, session_groups, sessions))
    1.27 -  }
    1.28 -
    1.29 -  def build_selection(
    1.30 -      options: Options,
    1.31 -      progress: Progress = No_Progress,
    1.32 -      build_heap: Boolean = false,
    1.33 -      clean_build: Boolean = false,
    1.34 -      dirs: List[Path] = Nil,
    1.35 -      select_dirs: List[Path] = Nil,
    1.36 -      numa_shuffling: Boolean = false,
    1.37 -      max_jobs: Int = 1,
    1.38 -      list_files: Boolean = false,
    1.39 -      check_keywords: Set[String] = Set.empty,
    1.40 -      no_build: Boolean = false,
    1.41 -      system_mode: Boolean = false,
    1.42 -      verbose: Boolean = false,
    1.43 -      pide: Boolean = false,
    1.44 -      selection: Sessions.Selection = Sessions.Selection.all): Results =
    1.45 +    sessions: List[String] = Nil,
    1.46 +    selection: Sessions.Selection = Sessions.Selection.empty): Results =
    1.47    {
    1.48      /* session selection and dependencies */
    1.49  
    1.50      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    1.51 +
    1.52      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    1.53 -    val (selected, selected_sessions) = full_sessions.selection(selection)
    1.54 +
    1.55 +    val (selected, selected_sessions) =
    1.56 +      full_sessions.selection(
    1.57 +          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    1.58 +            exclude_sessions, session_groups, sessions) + selection)
    1.59 +
    1.60      val deps =
    1.61        Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    1.62          verbose = verbose, list_files = list_files, check_keywords = check_keywords,