src/Pure/Tools/build.scala
changeset 59892 2a616319c171
parent 59891 9ce697050455
child 59893 89f3bd11fa8b
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 15:41:08 2015 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 16:24:38 2015 +0200
     1.3 @@ -162,12 +162,18 @@
     1.4      def apply(name: String): Session_Info = graph.get_node(name)
     1.5      def isDefinedAt(name: String): Boolean = graph.defined(name)
     1.6  
     1.7 -    def selection(requirements: Boolean, all_sessions: Boolean,
     1.8 -      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
     1.9 +    def selection(
    1.10 +      requirements: Boolean = false,
    1.11 +      all_sessions: Boolean = false,
    1.12 +      session_groups: List[String] = Nil,
    1.13 +      exclude_sessions: List[String] = Nil,
    1.14 +      sessions: List[String] = Nil): (List[String], Session_Tree) =
    1.15      {
    1.16 -      val bad_sessions = sessions.filterNot(isDefinedAt(_))
    1.17 +      val bad_sessions =
    1.18 +        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    1.19        if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    1.20  
    1.21 +      val excluded = graph.all_succs(exclude_sessions).toSet
    1.22        val pre_selected =
    1.23        {
    1.24          if (all_sessions) graph.keys
    1.25 @@ -179,7 +185,8 @@
    1.26              if info.select || select(name) || apply(name).groups.exists(select_group)
    1.27            } yield name).toList
    1.28          }
    1.29 -      }
    1.30 +      }.filterNot(excluded)
    1.31 +
    1.32        val selected =
    1.33          if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
    1.34          else pre_selected
    1.35 @@ -533,7 +540,7 @@
    1.36      dirs: List[Path],
    1.37      sessions: List[String]): Deps =
    1.38    {
    1.39 -    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
    1.40 +    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
    1.41      dependencies(inlined_files = inlined_files, tree = tree)
    1.42    }
    1.43  
    1.44 @@ -758,13 +765,14 @@
    1.45      no_build: Boolean = false,
    1.46      system_mode: Boolean = false,
    1.47      verbose: Boolean = false,
    1.48 +    exclude_sessions: List[String] = Nil,
    1.49      sessions: List[String] = Nil): Map[String, Int] =
    1.50    {
    1.51      /* session tree and dependencies */
    1.52  
    1.53      val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
    1.54      val (selected, selected_tree) =
    1.55 -      full_tree.selection(requirements, all_sessions, session_groups, sessions)
    1.56 +      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
    1.57  
    1.58      val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    1.59  
    1.60 @@ -1010,12 +1018,13 @@
    1.61      no_build: Boolean = false,
    1.62      system_mode: Boolean = false,
    1.63      verbose: Boolean = false,
    1.64 +    exclude_sessions: List[String] = Nil,
    1.65      sessions: List[String] = Nil): Int =
    1.66    {
    1.67      val results =
    1.68 -      build_results(options, progress, requirements, all_sessions,
    1.69 -        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
    1.70 -        list_files, check_keywords, no_build, system_mode, verbose, sessions)
    1.71 +      build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
    1.72 +        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
    1.73 +        no_build, system_mode, verbose, exclude_sessions, sessions)
    1.74  
    1.75      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    1.76      if (rc != 0 && (verbose || !no_build)) {
    1.77 @@ -1043,15 +1052,15 @@
    1.78            Properties.Value.Boolean(no_build) ::
    1.79            Properties.Value.Boolean(system_mode) ::
    1.80            Properties.Value.Boolean(verbose) ::
    1.81 -          Command_Line.Chunks(
    1.82 -              dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
    1.83 +          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
    1.84 +              build_options, exclude_sessions, sessions) =>
    1.85              val options = (Options.init() /: build_options)(_ + _)
    1.86              val progress = new Console_Progress(verbose)
    1.87              progress.interrupt_handler {
    1.88                build(options, progress, requirements, all_sessions, build_heap, clean_build,
    1.89                  dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
    1.90                  max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    1.91 -                verbose, sessions)
    1.92 +                verbose, exclude_sessions, sessions)
    1.93              }
    1.94          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.95        }