# HG changeset patch
# User wenzelm
# Date 1567626131 -7200
# Node ID d5e4231caa06a10d13a099c97b3f925e95a93065
# Parent  d1d4a1b1ff1f76a4c64504993a8cecc23ae5cd07
more complete graph;

diff -r d1d4a1b1ff1f -r d5e4231caa06 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Sep 04 20:05:57 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 04 21:42:11 2019 +0200
@@ -338,9 +338,20 @@
         case errs => error(cat_lines(errs))
       }
 
-    lazy val theory_graph: Document.Theory_Graph[A] =
-      Document.theory_graph(entries.map(entry =>
-        ((entry.name, seen(entry.name)), entry.header.imports)))
+    lazy val theory_graph: Document.Theory_Graph[Unit] =
+    {
+      val regular = theories.toSet
+      val irregular =
+        (for {
+          entry <- entries.iterator
+          imp <- entry.header.imports
+          if !regular(imp)
+        } yield imp).toSet
+
+      Document.theory_graph(
+        irregular.toList.map(name => ((name, ()), Nil)) :::
+        entries.map(entry => ((entry.name, ()), entry.header.imports)))
+    }
 
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>