src/Pure/Thy/sessions.scala
changeset 66823 f529719cc47d
parent 66822 4642cf4a7ebb
child 66828 3c936ebebc23
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 09 21:12:22 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 21:43:27 2017 +0200
     1.3 @@ -479,6 +479,9 @@
     1.4        val build_graph: Graph[String, Info],
     1.5        val imports_graph: Graph[String, Info])
     1.6    {
     1.7 +    def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     1.8 +    def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
     1.9 +
    1.10      def apply(name: String): Info = imports_graph.get_node(name)
    1.11      def get(name: String): Option[Info] =
    1.12        if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None