tuned: less oo-non-sense;
authorwenzelm
Mon Oct 09 22:03:05 2017 +0200 (19 months ago)
changeset 6682449a3a0a6ffaf
parent 66823 f529719cc47d
child 66825 9f6ec65f7a6e
tuned: less oo-non-sense;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Oct 09 21:43:27 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Oct 09 22:03:05 2017 +0200
     1.3 @@ -9,17 +9,13 @@
     1.4  
     1.5  object AFP
     1.6  {
     1.7 -  def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     1.8 -    new AFP(base_dir)
     1.9 +  def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    1.10 +    new AFP(options, base_dir)
    1.11  
    1.12    sealed case class Entry(name: String, sessions: List[String])
    1.13 -  {
    1.14 -    def sessions_deps(afp_sessions: Sessions.T): List[String] =
    1.15 -      sessions.flatMap(afp_sessions.imports_graph.imm_preds(_)).distinct.sorted
    1.16 -  }
    1.17  }
    1.18  
    1.19 -class AFP private(val base_dir: Path)
    1.20 +class AFP private(options: Options, val base_dir: Path)
    1.21  {
    1.22    override def toString: String = base_dir.expand.toString
    1.23  
    1.24 @@ -36,54 +32,46 @@
    1.25      }).sortBy(_.name)
    1.26  
    1.27    val sessions: List[String] = entries.flatMap(_.sessions)
    1.28 -  val sessions_set: Set[String] = sessions.toSet
    1.29 +
    1.30 +  val sessions_structure: Sessions.T =
    1.31 +    Sessions.load(options, dirs = List(main_dir)).
    1.32 +      selection(Sessions.Selection(sessions = sessions.toList))._2
    1.33  
    1.34  
    1.35 -  /* dependencies */
    1.36 +  /* dependency graph */
    1.37  
    1.38 -  def dependencies(options: Options): Dependencies =
    1.39 +  private def sessions_deps(entry: AFP.Entry): List[String] =
    1.40 +    entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
    1.41 +
    1.42 +  val entries_graph: Graph[String, Unit] =
    1.43    {
    1.44 -    val (_, afp_sessions) =
    1.45 -      Sessions.load(options, dirs = List(main_dir)).
    1.46 -        selection(Sessions.Selection(sessions = sessions.toList))
    1.47 -
    1.48      val session_entries =
    1.49        (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
    1.50          (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
    1.51        }
    1.52 -
    1.53 -    val entries_graph: Graph[String, Unit] =
    1.54 -      (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.55 -        val name1 = e1.name
    1.56 -        val g1 = g.default_node(name1, ())
    1.57 -        (g1 /: e1.sessions_deps(afp_sessions)) { case (g2, s2) =>
    1.58 -          (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.59 -            if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.60 -          }
    1.61 +    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.62 +      val name1 = e1.name
    1.63 +      val g1 = g.default_node(name1, ())
    1.64 +      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
    1.65 +        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.66 +          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.67          }
    1.68        }
    1.69 -
    1.70 -    new Dependencies(afp_sessions, entries_graph)
    1.71 +    }
    1.72    }
    1.73  
    1.74 -  final class Dependencies private [AFP](
    1.75 -    val afp_sessions: Sessions.T,
    1.76 -    val entries_graph: Graph[String, Unit])
    1.77 -  {
    1.78 -    def entries_graph_display: Graph_Display.Graph =
    1.79 -      Graph_Display.make_graph(entries_graph)
    1.80 +  def entries_graph_display: Graph_Display.Graph =
    1.81 +    Graph_Display.make_graph(entries_graph)
    1.82  
    1.83 -    def entries_json_text: String =
    1.84 -      (for (entry <- entries)
    1.85 -      yield {
    1.86 -        val distrib_deps = entry.sessions_deps(afp_sessions).filterNot(sessions_set)
    1.87 -        val afp_deps = entries_graph.imm_preds(entry.name).toList
    1.88 -        """
    1.89 +  def entries_json_text: String =
    1.90 +    (for (entry <- entries.iterator) yield {
    1.91 +      val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
    1.92 +      val afp_deps = entries_graph.imm_preds(entry.name).toList
    1.93 +      """
    1.94   {""" + JSON.Format(entry.name) + """:
    1.95    {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    1.96     "afp_deps": """ + JSON.Format(afp_deps) + """
    1.97    }
    1.98   }"""
    1.99 -      }).mkString("[", ", ", "\n]\n")
   1.100 -  }
   1.101 +    }).mkString("[", ", ", "\n]\n")
   1.102  }