--- 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)
+ }
}
-