# HG changeset patch
# User wenzelm
# Date 1507579385 -7200
# Node ID 49a3a0a6ffaf186f3f261c953799c58f18d3af45
# Parent  f529719cc47da7c83d07e9e902afdfc32c058590
tuned: less oo-non-sense;

diff -r f529719cc47d -r 49a3a0a6ffaf src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Oct 09 21:43:27 2017 +0200
+++ b/src/Pure/Admin/afp.scala	Mon Oct 09 22:03:05 2017 +0200
@@ -9,17 +9,13 @@
 
 object AFP
 {
-  def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP =
-    new AFP(base_dir)
+  def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
+    new AFP(options, base_dir)
 
   sealed case class Entry(name: String, sessions: List[String])
-  {
-    def sessions_deps(afp_sessions: Sessions.T): List[String] =
-      sessions.flatMap(afp_sessions.imports_graph.imm_preds(_)).distinct.sorted
-  }
 }
 
-class AFP private(val base_dir: Path)
+class AFP private(options: Options, val base_dir: Path)
 {
   override def toString: String = base_dir.expand.toString
 
@@ -36,54 +32,46 @@
     }).sortBy(_.name)
 
   val sessions: List[String] = entries.flatMap(_.sessions)
-  val sessions_set: Set[String] = sessions.toSet
+
+  val sessions_structure: Sessions.T =
+    Sessions.load(options, dirs = List(main_dir)).
+      selection(Sessions.Selection(sessions = sessions.toList))._2
 
 
-  /* dependencies */
+  /* dependency graph */
 
-  def dependencies(options: Options): Dependencies =
+  private def sessions_deps(entry: AFP.Entry): List[String] =
+    entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
+
+  val entries_graph: Graph[String, Unit] =
   {
-    val (_, afp_sessions) =
-      Sessions.load(options, dirs = List(main_dir)).
-        selection(Sessions.Selection(sessions = sessions.toList))
-
     val session_entries =
       (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
         (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
       }
-
-    val entries_graph: Graph[String, Unit] =
-      (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
-        val name1 = e1.name
-        val g1 = g.default_node(name1, ())
-        (g1 /: e1.sessions_deps(afp_sessions)) { case (g2, s2) =>
-          (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
-            if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
-          }
+    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
+      val name1 = e1.name
+      val g1 = g.default_node(name1, ())
+      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
+        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
+          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
         }
       }
-
-    new Dependencies(afp_sessions, entries_graph)
+    }
   }
 
-  final class Dependencies private [AFP](
-    val afp_sessions: Sessions.T,
-    val entries_graph: Graph[String, Unit])
-  {
-    def entries_graph_display: Graph_Display.Graph =
-      Graph_Display.make_graph(entries_graph)
+  def entries_graph_display: Graph_Display.Graph =
+    Graph_Display.make_graph(entries_graph)
 
-    def entries_json_text: String =
-      (for (entry <- entries)
-      yield {
-        val distrib_deps = entry.sessions_deps(afp_sessions).filterNot(sessions_set)
-        val afp_deps = entries_graph.imm_preds(entry.name).toList
-        """
+  def entries_json_text: String =
+    (for (entry <- entries.iterator) yield {
+      val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
+      val afp_deps = entries_graph.imm_preds(entry.name).toList
+      """
  {""" + JSON.Format(entry.name) + """:
   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    "afp_deps": """ + JSON.Format(afp_deps) + """
   }
  }"""
-      }).mkString("[", ", ", "\n]\n")
-  }
+    }).mkString("[", ", ", "\n]\n")
 }