more complete graph;
authorwenzelm
Wed, 04 Sep 2019 21:42:11 +0200
changeset 70842 d5e4231caa06
parent 70841 d1d4a1b1ff1f
child 70843 f7c5b30fc432
more complete graph;
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) =>