# HG changeset patch
# User wenzelm
# Date 1342706988 -7200
# Node ID a0b95a762abb167769e5f50fecd797f36a155f55
# Parent  09bf3b73e446c37b4a107c6a7ab31ae67c7bf42d
less redundant data structures;

diff -r 09bf3b73e446 -r a0b95a762abb src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 19 15:45:59 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 19 16:09:48 2012 +0200
@@ -40,15 +40,10 @@
 
     sealed case class Info(
       dir: Path,
-      key: Key,
-      parent: Option[String],
       description: String,
       options: Options,
       theories: List[(Options, String)],
       files: List[String])
-    {
-      def name: String = key.name
-    }
 
     object Queue
     {
@@ -59,19 +54,17 @@
       keys: Map[String, Key] = Map.empty,
       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
     {
-      def lookup(name: String): Option[Info] =
-        keys.get(name).map(graph.get_node(_))
+      def defined(name: String): Boolean = keys.isDefinedAt(name)
 
-      def + (info: Info): Queue =
+      def + (key: Key, info: Info, parent: Option[String]): Queue =
       {
         val keys1 =
-          if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name))
-          else keys + (info.name -> info.key)
+          if (defined(key.name)) error("Duplicate session: " + quote(key.name))
+          else keys + (key.name -> key)
 
         val graph1 =
           try {
-            graph.new_node(info.key, info).
-              add_deps_acyclic(info.key, info.parent.toList.map(keys(_)))
+            graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
           }
           catch {
             case exn: Graph.Cycles[_] =>
@@ -82,8 +75,8 @@
         new Queue(keys1, graph1)
       }
 
-      def topological_order: List[Info] =
-        graph.topological_order.map(graph.get_node(_))
+      def topological_order: List[(Key, Info)] =
+        graph.topological_order.map(key => (key, graph.get_node(key)))
     }
   }
 
@@ -176,13 +169,10 @@
           }
           else
             entry.parent match {
-              case None => error("Missing parent session")
-              case Some(parent) =>
-                val parent_info =
-                  sessions.lookup(parent) getOrElse
-                    error("Undefined parent session: " + quote(parent))
+              case Some(parent_name) if sessions.defined(parent_name) =>
                 if (entry.reset) entry.name
-                else parent_info.name + "-" + entry.name
+                else parent_name + "-" + entry.name
+              case _ => error("Bad parent session")
             }
 
         val path =
@@ -190,12 +180,12 @@
             case Some(p) => Path.explode(p)
             case None => Path.basic(entry.name)
           }
-        val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
-        val info =
-          Session.Info(dir + path, Session.Key(full_name, entry.order),
-            entry.parent, entry.description, entry.options, thys, entry.files)
 
-        sessions += info
+        val key = Session.Key(full_name, entry.order)
+        val info = Session.Info(dir + path, entry.description, entry.options,
+          entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
+
+        sessions += (key, info, entry.parent)
       }
       catch {
         case ERROR(msg) =>
@@ -217,8 +207,8 @@
     println("options = " + options.toString)
     println("sessions = " + sessions.toString)
 
-    for (info <- find_sessions(more_dirs).topological_order)
-      println(info.name + " in " + info.dir)
+    for ((key, info) <- find_sessions(more_dirs).topological_order)
+      println(key.name + " in " + info.dir)
 
     0
   }