src/Pure/System/build.scala
changeset 48595 231e6fa96dbb
parent 48594 c24907e5081e
child 48626 ef374008cb7c
--- a/src/Pure/System/build.scala	Mon Jul 30 11:03:44 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Jul 30 12:03:48 2012 +0200
@@ -64,14 +64,27 @@
 
       def - (name: String): Queue = new Queue(graph.del_node(name))
 
-      def required(groups: List[String], names: List[String]): Queue =
+      def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
+        : (List[String], Queue) =
       {
-        val selected_group = groups.toSet
-        val selected_name = names.toSet
+        sessions.filterNot(isDefinedAt(_)) match {
+          case Nil =>
+          case bad => error("Undefined session(s): " + commas_quote(bad))
+        }
+
         val selected =
-          graph.keys.filter(name =>
-            selected_name(name) || apply(name).groups.exists(selected_group)).toList
-        new Queue(graph.restrict(graph.all_preds(selected).toSet))
+        {
+          if (all_sessions) graph.keys.toList
+          else {
+            val sel_group = session_groups.toSet
+            val sel = sessions.toSet
+              graph.keys.toList.filter(name =>
+                sel(name) || apply(name).groups.exists(sel_group)).toList
+          }
+        }
+        val descendants = graph.all_succs(selected)
+        val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
+        (descendants, queue1)
       }
 
       def dequeue(skip: String => Boolean): Option[(String, Info)] =
@@ -83,7 +96,7 @@
       }
 
       def topological_order: List[(String, Info)] =
-        graph.topological_order.map(name => (name, graph.get_node(name)))
+        graph.topological_order.map(name => (name, apply(name)))
     }
   }
 
@@ -232,8 +245,7 @@
       })
   }
 
-  def find_sessions(options: Options, more_dirs: List[Path],
-    all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
+  def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
   {
     var queue = Session.Queue.empty
 
@@ -246,12 +258,7 @@
 
     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
 
-    sessions.filter(name => !queue.isDefinedAt(name)) match {
-      case Nil =>
-      case bad => error("Undefined session(s): " + commas_quote(bad))
-    }
-
-    if (all_sessions) queue else queue.required(session_groups, sessions)
+    queue
   }
 
 
@@ -439,6 +446,7 @@
   def build(
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
+    clean_build: Boolean = false,
     more_dirs: List[Path] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
@@ -449,7 +457,8 @@
     sessions: List[String] = Nil): Int =
   {
     val options = (Options.init() /: build_options)(_.define_simple(_))
-    val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
+    val (descendants, queue) =
+      find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
     val deps = dependencies(verbose, queue)
 
     def make_stamp(name: String): String =
@@ -469,6 +478,16 @@
     // prepare log dir
     (output_dir + LOG).file.mkdirs()
 
+    // optional cleanup
+    if (clean_build) {
+      for (name <- descendants) {
+        val files =
+          List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
+        if (!files.isEmpty) echo("Cleaning " + name + " ...")
+        if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
+      }
+    }
+
     // scheduler loop
     @tailrec def loop(
       pending: Session.Queue,
@@ -571,13 +590,14 @@
         case
           Properties.Value.Boolean(all_sessions) ::
           Properties.Value.Boolean(build_heap) ::
+          Properties.Value.Boolean(clean_build) ::
           Properties.Value.Int(max_jobs) ::
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
-            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
-              max_jobs, no_build, build_options, system_mode, verbose, sessions)
+            build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
+              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }