tuned signature;
authorwenzelm
Fri Apr 07 13:07:43 2017 +0200 (2017-04-07)
changeset 65422b606c98e6d10
parent 65421 6389e3ec32ec
child 65423 4527b33d5b3e
tuned signature;
src/Pure/Admin/ci_profile.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/ci_profile.scala	Fri Apr 07 11:53:44 2017 +0200
     1.2 +++ b/src/Pure/Admin/ci_profile.scala	Fri Apr 07 13:07:43 2017 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4      val progress = new Console_Progress(verbose = true)
     1.5      val start_time = Time.now()
     1.6      val results = progress.interrupt_handler {
     1.7 -      Build.build_selection(
     1.8 +      Build.build(
     1.9          options = options,
    1.10          progress = progress,
    1.11          clean_build = clean,
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 07 11:53:44 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 13:07:43 2017 +0200
     2.3 @@ -185,7 +185,7 @@
     2.4  
     2.5    object Selection
     2.6    {
     2.7 -    val all: Selection = Selection(all_sessions = true)
     2.8 +    val empty: Selection = Selection()
     2.9    }
    2.10  
    2.11    sealed case class Selection(
    2.12 @@ -196,6 +196,15 @@
    2.13      session_groups: List[String] = Nil,
    2.14      sessions: List[String] = Nil)
    2.15    {
    2.16 +    def + (other: Selection): Selection =
    2.17 +      Selection(
    2.18 +        requirements = requirements || other.requirements,
    2.19 +        all_sessions = all_sessions || other.all_sessions,
    2.20 +        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
    2.21 +        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
    2.22 +        session_groups = session_groups ::: other.session_groups,
    2.23 +        sessions = sessions ::: other.sessions)
    2.24 +
    2.25      def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    2.26      {
    2.27        val bad_sessions =
     3.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 11:53:44 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 13:07:43 2017 +0200
     3.3 @@ -351,50 +351,20 @@
     3.4      exclude_session_groups: List[String] = Nil,
     3.5      exclude_sessions: List[String] = Nil,
     3.6      session_groups: List[String] = Nil,
     3.7 -    sessions: List[String] = Nil): Results =
     3.8 -  {
     3.9 -    build_selection(
    3.10 -      options = options,
    3.11 -      progress = progress,
    3.12 -      build_heap = build_heap,
    3.13 -      clean_build = clean_build,
    3.14 -      dirs = dirs,
    3.15 -      select_dirs = select_dirs,
    3.16 -      numa_shuffling = numa_shuffling,
    3.17 -      max_jobs = max_jobs,
    3.18 -      list_files = list_files,
    3.19 -      check_keywords = check_keywords,
    3.20 -      no_build = no_build,
    3.21 -      system_mode = system_mode,
    3.22 -      verbose = verbose,
    3.23 -      pide = pide,
    3.24 -      selection =
    3.25 -        Sessions.Selection(requirements, all_sessions,
    3.26 -          exclude_session_groups, exclude_sessions, session_groups, sessions))
    3.27 -  }
    3.28 -
    3.29 -  def build_selection(
    3.30 -      options: Options,
    3.31 -      progress: Progress = No_Progress,
    3.32 -      build_heap: Boolean = false,
    3.33 -      clean_build: Boolean = false,
    3.34 -      dirs: List[Path] = Nil,
    3.35 -      select_dirs: List[Path] = Nil,
    3.36 -      numa_shuffling: Boolean = false,
    3.37 -      max_jobs: Int = 1,
    3.38 -      list_files: Boolean = false,
    3.39 -      check_keywords: Set[String] = Set.empty,
    3.40 -      no_build: Boolean = false,
    3.41 -      system_mode: Boolean = false,
    3.42 -      verbose: Boolean = false,
    3.43 -      pide: Boolean = false,
    3.44 -      selection: Sessions.Selection = Sessions.Selection.all): Results =
    3.45 +    sessions: List[String] = Nil,
    3.46 +    selection: Sessions.Selection = Sessions.Selection.empty): Results =
    3.47    {
    3.48      /* session selection and dependencies */
    3.49  
    3.50      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    3.51 +
    3.52      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    3.53 -    val (selected, selected_sessions) = full_sessions.selection(selection)
    3.54 +
    3.55 +    val (selected, selected_sessions) =
    3.56 +      full_sessions.selection(
    3.57 +          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    3.58 +            exclude_sessions, session_groups, sessions) + selection)
    3.59 +
    3.60      val deps =
    3.61        Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    3.62          verbose = verbose, list_files = list_files, check_keywords = check_keywords,