src/Pure/Thy/thy_info.scala
changeset 65507 decdb95bd007
parent 65471 05e5bffcf1d8
child 66695 91500c024c7f
--- a/src/Pure/Thy/thy_info.scala	Tue Apr 18 19:14:01 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Apr 18 19:17:46 2017 +0200
@@ -101,26 +101,6 @@
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }
 
-    def session_graph(parent_session: String, parent_base: Sessions.Base): Graph_Display.Graph =
-    {
-      val parent_session_node =
-        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
-
-      def node(name: Document.Node.Name): Graph_Display.Node =
-        if (parent_base.loaded_theory(name)) parent_session_node
-        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
-
-      (Graph_Display.empty_graph /: deps) {
-        case (g, dep) =>
-          if (parent_base.loaded_theory(dep.name)) g
-          else {
-            val a = node(dep.name)
-            val bs = dep.header.imports.map({ case (name, _) => node(name) })
-            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
-          }
-      }
-    }
-
     override def toString: String = deps.toString
   }