restrict to required sessions;
authorwenzelm
Fri, 20 Jul 2012 12:27:25 +0200
changeset 48363 cf081b7042d2
parent 48362 c3192ccb0ff4
child 48364 9091b659d7b6
restrict to required sessions;
src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 20 12:00:08 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 12:27:25 2012 +0200
@@ -75,6 +75,14 @@
         new Queue(keys1, graph1)
       }
 
+      def required(names: List[String]): Queue =
+      {
+        val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
+        val keys1 = keys -- keys.keySet.filter(name => !req(name))
+        val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
+        new Queue(keys1, graph1)
+      }
+
       def topological_order: List[(Key, Info)] =
         graph.topological_order.map(key => (key, graph.get_node(key)))
     }
@@ -235,11 +243,18 @@
   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
     more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
   {
-    println("more_dirs = " + more_dirs.toString)
-    println("options = " + options.toString)
-    println("sessions = " + sessions.toString)
+    val full_queue = find_sessions(more_dirs)
 
-    for ((key, info) <- find_sessions(more_dirs).topological_order)
+    sessions.filter(name => !full_queue.defined(name)) match {
+      case Nil =>
+      case bad => error("Undefined session(s): " + commas_quote(bad))
+    }
+
+    val required_queue =
+      if (all_sessions) full_queue
+      else full_queue.required(sessions)
+
+    for ((key, info) <- required_queue.topological_order)
       println(key.name + " in " + info.dir)
 
     0