# HG changeset patch
# User wenzelm
# Date 1343913808 -7200
# Node ID bf9bff84a61d2ab5e87f29f365d6d79192ce9149
# Parent  f13eeeea1a69be87a73ba5906dff48efc3b533ca
allow session specifications in arbitrary order;

diff -r f13eeeea1a69 -r bf9bff84a61d src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Aug 02 15:05:32 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Aug 02 15:23:28 2012 +0200
@@ -41,32 +41,50 @@
       val empty: Queue = new Queue()
     }
 
-    final class Queue private(graph: Graph[String, Info] = Graph.string)
+    final class Queue private(graph: Graph[String, Option[Info]] = Graph.string)
       extends PartialFunction[String, Info]
     {
-      def apply(name: String): Info = graph.get_node(name)
-      def isDefinedAt(name: String): Boolean = graph.defined(name)
+      def apply(name: String): Info = graph.get_node(name).get
+      def isDefinedAt(name: String): Boolean =
+        graph.defined(name) && graph.get_node(name).isDefined
 
       def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
       def is_empty: Boolean = graph.is_empty
 
       def + (name: String, info: Info): Queue =
+      {
+        val parents = info.parent.toList
+
+        val graph1 = (graph /: (name :: parents))(_.default_node(_, None))
+        if (graph1.get_node(name).isDefined)
+          error("Duplicate session: " + quote(name))
+
         new Queue(
-          try { graph.new_node(name, info).add_deps_acyclic(name, info.parent.toList) }
+          try { graph1.map_node(name, _ => Some(info)).add_deps_acyclic(name, parents) }
           catch {
-            case _: Graph.Duplicate[_] => error("Duplicate session: " + quote(name))
             case exn: Graph.Cycles[_] =>
               error(cat_lines(exn.cycles.map(cycle =>
                 "Cyclic session dependency of " +
                   cycle.map(c => quote(c.toString)).mkString(" via "))))
           })
+      }
 
       def - (name: String): Queue = new Queue(graph.del_node(name))
 
       def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
         : (List[String], Queue) =
       {
+        (for {
+          (name, (Some(info), _)) <- graph.entries
+          if info.parent.isDefined; parent = info.parent.get
+          if !isDefinedAt(parent)
+        } yield parent + " (for " + name + ")").toList match
+        {
+          case Nil =>
+          case bad => error("Bad parent session(s): " + commas(bad))
+        }
+
         sessions.filterNot(isDefinedAt(_)) match {
           case Nil =>
           case bad => error("Undefined session(s): " + commas_quote(bad))
@@ -90,8 +108,8 @@
       def dequeue(skip: String => Boolean): Option[(String, Info)] =
       {
         val it = graph.entries.dropWhile(
-          { case (name, (_, (deps, _))) => !deps.isEmpty || skip(name) })
-        if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info)) }
+          { case (name, (info, (deps, _))) => !deps.isEmpty || info.isEmpty || skip(name) })
+        if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info.get)) }
         else None
       }
 
@@ -183,12 +201,10 @@
           }
           else
             entry.parent match {
-              case Some(parent_name) if queue1.isDefinedAt(parent_name) =>
-                val full_name =
-                  if (entry.this_name) entry.base_name
-                  else parent_name + "-" + entry.base_name
-                full_name
-              case _ => error("Bad parent session")
+              case None => error("Missing parent session")
+              case Some(parent_name) =>
+                if (entry.this_name) entry.base_name
+                else parent_name + "-" + entry.base_name
             }
 
         val path =