--- 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) =>