author | wenzelm |
Tue, 10 Oct 2017 19:23:03 +0200 | |
changeset 66831 | 29ea2b900a05 |
parent 66824 | 49a3a0a6ffaf |
child 66832 | 875fe2cb7e70 |
permissions | -rw-r--r-- |
66820 | 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 |
{ |
|
66824 | 12 |
def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = |
13 |
new AFP(options, base_dir) |
|
66820 | 14 |
|
66821 | 15 |
sealed case class Entry(name: String, sessions: List[String]) |
66820 | 16 |
} |
17 |
||
66824 | 18 |
class AFP private(options: Options, val base_dir: Path) |
66820 | 19 |
{ |
66821 | 20 |
override def toString: String = base_dir.expand.toString |
21 |
||
66820 | 22 |
val main_dir: Path = base_dir + Path.explode("thys") |
23 |
||
66821 | 24 |
|
25 |
/* entries and sessions */ |
|
26 |
||
66820 | 27 |
val entries: List[AFP.Entry] = |
66821 | 28 |
(for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield { |
66820 | 29 |
val sessions = |
30 |
Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name) |
|
31 |
AFP.Entry(name, sessions) |
|
32 |
}).sortBy(_.name) |
|
33 |
||
66821 | 34 |
val sessions: List[String] = entries.flatMap(_.sessions) |
66824 | 35 |
|
36 |
val sessions_structure: Sessions.T = |
|
37 |
Sessions.load(options, dirs = List(main_dir)). |
|
38 |
selection(Sessions.Selection(sessions = sessions.toList))._2 |
|
66821 | 39 |
|
40 |
||
66824 | 41 |
/* dependency graph */ |
66821 | 42 |
|
66824 | 43 |
private def sessions_deps(entry: AFP.Entry): List[String] = |
44 |
entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted |
|
45 |
||
46 |
val entries_graph: Graph[String, Unit] = |
|
66821 | 47 |
{ |
48 |
val session_entries = |
|
66831
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
49 |
(Map.empty[String, String] /: entries) { |
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
50 |
case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) } |
66821 | 51 |
} |
66831
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
52 |
(Graph.empty[String, Unit] /: entries) { case (g, entry) => |
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
53 |
val e1 = entry.name |
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
54 |
(g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s2) => |
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
55 |
(g1 /: session_entries.get(s2).filterNot(_ == e1)) { case (g2, e2) => |
29ea2b900a05
tuned: each session has at most one defining entry;
wenzelm
parents:
66824
diff
changeset
|
56 |
g2.default_node(e2, ()).add_edge(e2, e1) |
66821 | 57 |
} |
58 |
} |
|
66824 | 59 |
} |
66821 | 60 |
} |
61 |
||
66824 | 62 |
def entries_graph_display: Graph_Display.Graph = |
63 |
Graph_Display.make_graph(entries_graph) |
|
66823 | 64 |
|
66824 | 65 |
def entries_json_text: String = |
66 |
(for (entry <- entries.iterator) yield { |
|
67 |
val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_)) |
|
68 |
val afp_deps = entries_graph.imm_preds(entry.name).toList |
|
69 |
""" |
|
66821 | 70 |
{""" + JSON.Format(entry.name) + """: |
71 |
{"distrib_deps": """ + JSON.Format(distrib_deps) + """, |
|
72 |
"afp_deps": """ + JSON.Format(afp_deps) + """ |
|
73 |
} |
|
74 |
}""" |
|
66824 | 75 |
}).mkString("[", ", ", "\n]\n") |
66820 | 76 |
} |