# HG changeset patch
# User wenzelm
# Date 1422213740 -3600
# Node ID d57e275b2d82b11f5fe6d721a67d484104dce398
# Parent  5b552b4f63a5eaa1fc894733f6e6db85f6d06258
support for session graph from Scala side;

diff -r 5b552b4f63a5 -r d57e275b2d82 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Sun Jan 25 20:16:27 2015 +0100
+++ b/src/Pure/Thy/thy_info.scala	Sun Jan 25 20:22:20 2015 +0100
@@ -91,6 +91,26 @@
           rev_deps)
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }
+
+    def deps_graph(parent_session: String, parent_loaded: String => Boolean): 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_loaded(name.theory)) parent_session_node
+        else Graph_Display.Node(name.theory, "theory." + name.theory)
+
+      (Graph_Display.empty_graph /: rev_deps) {
+        case (g, dep) =>
+          if (parent_loaded(dep.name.theory)) g
+          else {
+            val a = node(dep.name)
+            val bs = dep.header.imports.map(node _)
+            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
+          }
+      }
+    }
   }
 
   private def require_thys(session: String, initiators: List[Document.Node.Name],
diff -r 5b552b4f63a5 -r d57e275b2d82 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jan 25 20:16:27 2015 +0100
+++ b/src/Pure/Tools/build.scala	Sun Jan 25 20:22:20 2015 +0100
@@ -416,7 +416,8 @@
     known_theories: Map[String, Document.Node.Name],
     keywords: Thy_Header.Keywords,
     syntax: Outer_Syntax,
-    sources: List[(Path, SHA1.Digest)])
+    sources: List[(Path, SHA1.Digest)],
+    session_graph: Graph_Display.Graph)
 
   sealed case class Deps(deps: Map[String, Session_Content])
   {
@@ -494,8 +495,11 @@
 
             val sources = all_files.map(p => (p, SHA1.digest(p.file)))
 
+            val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
+
             val content =
-              Session_Content(loaded_theories, known_theories, keywords, syntax, sources)
+              Session_Content(loaded_theories, known_theories, keywords, syntax,
+                sources, session_graph)
             deps + (name -> content)
           }
           catch {