--- 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 =