# HG changeset patch # User wenzelm # Date 1464955871 -7200 # Node ID 78e93610a3c8cd30acb23a1cbafd9bd4cf115562 # Parent bcf4828bb125a0d0e648f592808ef3723b1c9026 more flexible build_selection; diff -r bcf4828bb125 -r 78e93610a3c8 src/Pure/Tools/build.scala --- 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