src/Pure/Tools/build.scala
changeset 60106 e0d1d9203275
parent 60077 55cb9462e602
child 60215 5fb4990dfc73
     1.1 --- a/src/Pure/Tools/build.scala	Fri Apr 17 09:56:12 2015 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 17 11:28:57 2015 +0200
     1.3 @@ -165,15 +165,26 @@
     1.4      def selection(
     1.5        requirements: Boolean = false,
     1.6        all_sessions: Boolean = false,
     1.7 +      exclude_session_groups: List[String] = Nil,
     1.8 +      exclude_sessions: List[String] = Nil,
     1.9        session_groups: List[String] = Nil,
    1.10 -      exclude_sessions: List[String] = Nil,
    1.11        sessions: List[String] = Nil): (List[String], Session_Tree) =
    1.12      {
    1.13        val bad_sessions =
    1.14          SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    1.15        if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    1.16  
    1.17 -      val excluded = graph.all_succs(exclude_sessions).toSet
    1.18 +      val excluded =
    1.19 +      {
    1.20 +        val exclude_group = exclude_session_groups.toSet
    1.21 +        val exclude_group_sessions =
    1.22 +          (for {
    1.23 +            (name, (info, _)) <- graph.iterator
    1.24 +            if apply(name).groups.exists(exclude_group)
    1.25 +          } yield name).toList
    1.26 +        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
    1.27 +      }
    1.28 +
    1.29        val pre_selected =
    1.30        {
    1.31          if (all_sessions) graph.keys
    1.32 @@ -751,6 +762,7 @@
    1.33      clean_build: Boolean = false,
    1.34      dirs: List[Path] = Nil,
    1.35      select_dirs: List[Path] = Nil,
    1.36 +    exclude_session_groups: List[String] = Nil,
    1.37      session_groups: List[String] = Nil,
    1.38      max_jobs: Int = 1,
    1.39      list_files: Boolean = false,
    1.40 @@ -765,7 +777,8 @@
    1.41  
    1.42      val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
    1.43      val (selected, selected_tree) =
    1.44 -      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
    1.45 +      full_tree.selection(requirements, all_sessions,
    1.46 +        exclude_session_groups, exclude_sessions, session_groups, sessions)
    1.47  
    1.48      val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    1.49  
    1.50 @@ -1004,6 +1017,7 @@
    1.51      clean_build: Boolean = false,
    1.52      dirs: List[Path] = Nil,
    1.53      select_dirs: List[Path] = Nil,
    1.54 +    exclude_session_groups: List[String] = Nil,
    1.55      session_groups: List[String] = Nil,
    1.56      max_jobs: Int = 1,
    1.57      list_files: Boolean = false,
    1.58 @@ -1016,8 +1030,8 @@
    1.59    {
    1.60      val results =
    1.61        build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
    1.62 -        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
    1.63 -        no_build, system_mode, verbose, exclude_sessions, sessions)
    1.64 +        dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
    1.65 +        check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
    1.66  
    1.67      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    1.68      if (rc != 0 && (verbose || !no_build)) {
    1.69 @@ -1046,13 +1060,13 @@
    1.70            Properties.Value.Boolean(system_mode) ::
    1.71            Properties.Value.Boolean(verbose) ::
    1.72            Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
    1.73 -              build_options, exclude_sessions, sessions) =>
    1.74 +              build_options, exclude_session_groups, exclude_sessions, sessions) =>
    1.75              val options = (Options.init() /: build_options)(_ + _)
    1.76              val progress = new Console_Progress(verbose)
    1.77              progress.interrupt_handler {
    1.78                build(options, progress, requirements, all_sessions, build_heap, clean_build,
    1.79 -                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
    1.80 -                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    1.81 +                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
    1.82 +                session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    1.83                  verbose, exclude_sessions, sessions)
    1.84              }
    1.85          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.86 @@ -1116,4 +1130,3 @@
    1.87          Markup.LOADING_THEORY -> loading_theory _)
    1.88    }
    1.89  }
    1.90 -