src/Pure/System/build.scala
changeset 48595 231e6fa96dbb
parent 48594 c24907e5081e
child 48626 ef374008cb7c
     1.1 --- a/src/Pure/System/build.scala	Mon Jul 30 11:03:44 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Mon Jul 30 12:03:48 2012 +0200
     1.3 @@ -64,14 +64,27 @@
     1.4  
     1.5        def - (name: String): Queue = new Queue(graph.del_node(name))
     1.6  
     1.7 -      def required(groups: List[String], names: List[String]): Queue =
     1.8 +      def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
     1.9 +        : (List[String], Queue) =
    1.10        {
    1.11 -        val selected_group = groups.toSet
    1.12 -        val selected_name = names.toSet
    1.13 +        sessions.filterNot(isDefinedAt(_)) match {
    1.14 +          case Nil =>
    1.15 +          case bad => error("Undefined session(s): " + commas_quote(bad))
    1.16 +        }
    1.17 +
    1.18          val selected =
    1.19 -          graph.keys.filter(name =>
    1.20 -            selected_name(name) || apply(name).groups.exists(selected_group)).toList
    1.21 -        new Queue(graph.restrict(graph.all_preds(selected).toSet))
    1.22 +        {
    1.23 +          if (all_sessions) graph.keys.toList
    1.24 +          else {
    1.25 +            val sel_group = session_groups.toSet
    1.26 +            val sel = sessions.toSet
    1.27 +              graph.keys.toList.filter(name =>
    1.28 +                sel(name) || apply(name).groups.exists(sel_group)).toList
    1.29 +          }
    1.30 +        }
    1.31 +        val descendants = graph.all_succs(selected)
    1.32 +        val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
    1.33 +        (descendants, queue1)
    1.34        }
    1.35  
    1.36        def dequeue(skip: String => Boolean): Option[(String, Info)] =
    1.37 @@ -83,7 +96,7 @@
    1.38        }
    1.39  
    1.40        def topological_order: List[(String, Info)] =
    1.41 -        graph.topological_order.map(name => (name, graph.get_node(name)))
    1.42 +        graph.topological_order.map(name => (name, apply(name)))
    1.43      }
    1.44    }
    1.45  
    1.46 @@ -232,8 +245,7 @@
    1.47        })
    1.48    }
    1.49  
    1.50 -  def find_sessions(options: Options, more_dirs: List[Path],
    1.51 -    all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
    1.52 +  def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
    1.53    {
    1.54      var queue = Session.Queue.empty
    1.55  
    1.56 @@ -246,12 +258,7 @@
    1.57  
    1.58      for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
    1.59  
    1.60 -    sessions.filter(name => !queue.isDefinedAt(name)) match {
    1.61 -      case Nil =>
    1.62 -      case bad => error("Undefined session(s): " + commas_quote(bad))
    1.63 -    }
    1.64 -
    1.65 -    if (all_sessions) queue else queue.required(session_groups, sessions)
    1.66 +    queue
    1.67    }
    1.68  
    1.69  
    1.70 @@ -439,6 +446,7 @@
    1.71    def build(
    1.72      all_sessions: Boolean = false,
    1.73      build_heap: Boolean = false,
    1.74 +    clean_build: Boolean = false,
    1.75      more_dirs: List[Path] = Nil,
    1.76      session_groups: List[String] = Nil,
    1.77      max_jobs: Int = 1,
    1.78 @@ -449,7 +457,8 @@
    1.79      sessions: List[String] = Nil): Int =
    1.80    {
    1.81      val options = (Options.init() /: build_options)(_.define_simple(_))
    1.82 -    val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
    1.83 +    val (descendants, queue) =
    1.84 +      find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
    1.85      val deps = dependencies(verbose, queue)
    1.86  
    1.87      def make_stamp(name: String): String =
    1.88 @@ -469,6 +478,16 @@
    1.89      // prepare log dir
    1.90      (output_dir + LOG).file.mkdirs()
    1.91  
    1.92 +    // optional cleanup
    1.93 +    if (clean_build) {
    1.94 +      for (name <- descendants) {
    1.95 +        val files =
    1.96 +          List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
    1.97 +        if (!files.isEmpty) echo("Cleaning " + name + " ...")
    1.98 +        if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
    1.99 +      }
   1.100 +    }
   1.101 +
   1.102      // scheduler loop
   1.103      @tailrec def loop(
   1.104        pending: Session.Queue,
   1.105 @@ -571,13 +590,14 @@
   1.106          case
   1.107            Properties.Value.Boolean(all_sessions) ::
   1.108            Properties.Value.Boolean(build_heap) ::
   1.109 +          Properties.Value.Boolean(clean_build) ::
   1.110            Properties.Value.Int(max_jobs) ::
   1.111            Properties.Value.Boolean(no_build) ::
   1.112            Properties.Value.Boolean(system_mode) ::
   1.113            Properties.Value.Boolean(verbose) ::
   1.114            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   1.115 -            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
   1.116 -              max_jobs, no_build, build_options, system_mode, verbose, sessions)
   1.117 +            build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
   1.118 +              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
   1.119          case _ => error("Bad arguments:\n" + cat_lines(args))
   1.120        }
   1.121      }