# HG changeset patch
# User wenzelm
# Date 1507578207 -7200
# Node ID f529719cc47da7c83d07e9e902afdfc32c058590
# Parent  4642cf4a7ebbcef9ce46046149e52c6d04534f95
operations for graph display;

diff -r 4642cf4a7ebb -r f529719cc47d src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon Oct 09 21:12:22 2017 +0200
+++ b/src/Pure/Admin/afp.scala	Mon Oct 09 21:43:27 2017 +0200
@@ -70,6 +70,9 @@
     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_json_text: String =
       (for (entry <- entries)
       yield {
diff -r 4642cf4a7ebb -r f529719cc47d src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Mon Oct 09 21:12:22 2017 +0200
+++ b/src/Pure/General/graph_display.scala	Mon Oct 09 21:43:27 2017 +0200
@@ -60,5 +60,13 @@
         import XML.Decode._
         list(pair(pair(string, pair(string, x => x)), list(string)))(body)
       })
+
+  def make_graph[A](
+    graph: isabelle.Graph[String, A],
+    name: (String, A) => String = (x: String, a: A) => x): Graph =
+  {
+    val entries =
+      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
+    build_graph(entries)
+  }
 }
-
diff -r 4642cf4a7ebb -r f529719cc47d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 09 21:12:22 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 21:43:27 2017 +0200
@@ -479,6 +479,9 @@
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
+    def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
+    def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
+
     def apply(name: String): Info = imports_graph.get_node(name)
     def get(name: String): Option[Info] =
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None