# HG changeset patch
# User wenzelm
# Date 1492535866 -7200
# Node ID decdb95bd007903b192b8452ff2b2f4f8ba33c45
# Parent  359fc6266a008af363fcbc126925826c30a3989d
clarified session graph: collapse theories from other sessions;

diff -r 359fc6266a00 -r decdb95bd007 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 18 19:14:01 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 18 19:17:46 2017 +0200
@@ -204,6 +204,39 @@
             if (check_keywords.nonEmpty)
               Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
 
+            val session_graph: Graph_Display.Graph =
+            {
+              def session_node(name: String): Graph_Display.Node =
+                Graph_Display.Node("[" + name + "]", "session." + name)
+
+              def node(name: Document.Node.Name): Graph_Display.Node =
+              {
+                val session = resources.theory_qualifier(name)
+                if (session == session_name)
+                  Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
+                else session_node(session)
+              }
+
+              val imports_subgraph =
+                sessions.imports_graph.restrict(
+                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
+
+              val graph0 =
+                (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
+                  { case (g, session) =>
+                      val a = session_node(session)
+                      val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
+                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+
+              (graph0 /: thy_deps.deps)(
+                { case (g, dep) =>
+                    val a = node(dep.name)
+                    val bs =
+                      dep.header.imports.map({ case (name, _) => node(name) }).
+                        filterNot(_ == a)
+                    ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+            }
+
             val base =
               Base(global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
@@ -211,7 +244,7 @@
                 keywords = thy_deps.keywords,
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
-                session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
+                session_graph = session_graph)
 
             session_bases + (session_name -> base)
           }
diff -r 359fc6266a00 -r decdb95bd007 src/Pure/Thy/thy_info.scala
--- 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
   }