src/Pure/Admin/afp.scala
author wenzelm
Mon Oct 09 21:43:27 2017 +0200 (22 months ago)
changeset 66823 f529719cc47d
parent 66821 c0e8c199cb2e
child 66824 49a3a0a6ffaf
permissions -rw-r--r--
operations for graph display;
     1 /*  Title:      Pure/Admin/afp.scala
     2     Author:     Makarius
     3 
     4 Administrative support for the Archive of Formal Proofs.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object AFP
    11 {
    12   def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    13     new AFP(base_dir)
    14 
    15   sealed case class Entry(name: String, sessions: List[String])
    16   {
    17     def sessions_deps(afp_sessions: Sessions.T): List[String] =
    18       sessions.flatMap(afp_sessions.imports_graph.imm_preds(_)).distinct.sorted
    19   }
    20 }
    21 
    22 class AFP private(val base_dir: Path)
    23 {
    24   override def toString: String = base_dir.expand.toString
    25 
    26   val main_dir: Path = base_dir + Path.explode("thys")
    27 
    28 
    29   /* entries and sessions */
    30 
    31   val entries: List[AFP.Entry] =
    32     (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    33       val sessions =
    34         Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    35       AFP.Entry(name, sessions)
    36     }).sortBy(_.name)
    37 
    38   val sessions: List[String] = entries.flatMap(_.sessions)
    39   val sessions_set: Set[String] = sessions.toSet
    40 
    41 
    42   /* dependencies */
    43 
    44   def dependencies(options: Options): Dependencies =
    45   {
    46     val (_, afp_sessions) =
    47       Sessions.load(options, dirs = List(main_dir)).
    48         selection(Sessions.Selection(sessions = sessions.toList))
    49 
    50     val session_entries =
    51       (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
    52         (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
    53       }
    54 
    55     val entries_graph: Graph[String, Unit] =
    56       (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    57         val name1 = e1.name
    58         val g1 = g.default_node(name1, ())
    59         (g1 /: e1.sessions_deps(afp_sessions)) { case (g2, s2) =>
    60           (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    61             if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    62           }
    63         }
    64       }
    65 
    66     new Dependencies(afp_sessions, entries_graph)
    67   }
    68 
    69   final class Dependencies private [AFP](
    70     val afp_sessions: Sessions.T,
    71     val entries_graph: Graph[String, Unit])
    72   {
    73     def entries_graph_display: Graph_Display.Graph =
    74       Graph_Display.make_graph(entries_graph)
    75 
    76     def entries_json_text: String =
    77       (for (entry <- entries)
    78       yield {
    79         val distrib_deps = entry.sessions_deps(afp_sessions).filterNot(sessions_set)
    80         val afp_deps = entries_graph.imm_preds(entry.name).toList
    81         """
    82  {""" + JSON.Format(entry.name) + """:
    83   {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    84    "afp_deps": """ + JSON.Format(afp_deps) + """
    85   }
    86  }"""
    87       }).mkString("[", ", ", "\n]\n")
    88   }
    89 }