# HG changeset patch
# User wenzelm
# Date 1527535743 -7200
# Node ID 812546f20c5cde45c308b2d4d789bfe00d0006bf
# Parent  d575281e18d087ec09cf0e5c5e0a0c093b765094
more accurate theory_graph: avoid imports of loaded_theories with incomplete node name;

diff -r d575281e18d0 -r 812546f20c5c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon May 28 17:40:34 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon May 28 21:29:03 2018 +0200
@@ -120,19 +120,10 @@
 
     lazy val theory_graph: Graph[Document.Node.Name, Unit] =
     {
-      val graph0 =
-        (Graph.empty[Document.Node.Name, Unit](Document.Node.Name.Ordering) /: theories)(
-          {
-            case (g1, (_, entry)) =>
-              (g1.default_node(entry.name, ()) /: entry.header.imports)(
-                { case (g2, (parent, _)) => g2.default_node(parent, ()) })
-          })
-      (graph0 /: theories)(
-        {
-          case (g1, (_, entry)) =>
-            (g1 /: entry.header.imports)(
-              { case (g2, (parent, _)) => g2.add_edge(parent, entry.name) })
-        })
+      val entries =
+        for ((_, entry) <- theories.toList)
+        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp._1.theory).name))
+      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
     }
 
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
@@ -375,7 +366,10 @@
           }
       })
 
-    Deps(sessions_structure, session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
+    val all_known =
+      Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_)))
+
+    Deps(sessions_structure, session_bases, all_known)
   }