clarified signature: full dependency graph;

--- a/src/Pure/General/graph.scala	Sat Aug 31 21:34:39 2019 +0200
+++ b/src/Pure/General/graph.scala	Sun Sep 01 22:57:25 2019 +0200
@@ -20,11 +20,14 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])], symmetric: Boolean = false)(
-    implicit ord: Ordering[Key]): Graph[Key, A] =
+  def make[Key, A](entries: List[((Key, A), List[Key])],
+    symmetric: Boolean = false,
+    permissive: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
-      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
+      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) =>
+        if (permissive) graph.default_node(x, info) else graph.new_node(x, info)
+      }
     val graph2 =
       (graph1 /: entries) { case (graph, ((x, _), ys)) =>
         (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }

--- a/src/Pure/PIDE/document.scala	Sat Aug 31 21:34:39 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 01 22:57:25 2019 +0200
@@ -106,6 +106,11 @@
       {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
+
+      object Theory_Ordering extends scala.math.Ordering[Name]
+      {
+        def compare(name1: Name, name2: Name): Int = name1.theory compare name2.theory
+      }
     }
 
     sealed case class Name(node: String, master_dir: String = "", theory: String = "")
@@ -136,6 +141,8 @@
     {
       def map(f: String => String): Entry = copy(name = name.map(f))
 
+      def imports: List[Node.Name] = header.imports.map(_._1)
+
       override def toString: String = name.toString
     }
 

--- a/src/Pure/PIDE/headless.scala	Sat Aug 31 21:34:39 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 01 22:57:25 2019 +0200
@@ -492,8 +492,8 @@
       deps: Sessions.Deps, progress: Progress = No_Progress): List[Document.Node.Name] =
     {
       for {
-        (_, name) <- deps.used_theories_condition(options, progress = progress)
-        if !session_base.loaded_theory(name)
+        name <- deps.used_theories_condition(options, progress = progress).topological_order
+        if !session_base.loaded_theory(name.theory)
       } yield name
     }
 

--- a/src/Pure/Thy/sessions.scala	Sat Aug 31 21:34:39 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Sep 01 22:57:25 2019 +0200
@@ -147,7 +147,7 @@
     doc_names: List[String] = Nil,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
-    used_theories: List[(Options, Document.Node.Name)] = Nil,
+    used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil,
     dump_checkpoint: List[Document.Node.Name] = Nil,
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -208,30 +208,33 @@
       } yield name).toList
 
     def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
-      : List[(Options, Document.Node.Name)] =
+      : Graph[Document.Node.Name, Options] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
-      for {
-        session_name <- sessions_structure.build_topological_order
-        (options, name) <- session_bases(session_name).used_theories
-        if {
-          def warn(msg: String): Unit =
-            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
+      val used =
+        for {
+          session_name <- sessions_structure.build_topological_order
+          entry @ ((name, options), _) <- session_bases(session_name).used_theories
+          if {
+            def warn(msg: String): Unit =
+              progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
 
-          val conditions =
-            space_explode(',', options.string("condition")).
-              filter(cond => Isabelle_System.getenv(cond) == "")
-          if (conditions.nonEmpty) {
-            warn("undefined " + conditions.mkString(", "))
-            false
+            val conditions =
+              space_explode(',', options.string("condition")).
+                filter(cond => Isabelle_System.getenv(cond) == "")
+            if (conditions.nonEmpty) {
+              warn("undefined " + conditions.mkString(", "))
+              false
+            }
+            else if (default_skip_proofs && !options.bool("skip_proofs")) {
+              warn("option skip_proofs")
+              false
+            }
+            else true
           }
-          else if (default_skip_proofs && !options.bool("skip_proofs")) {
-            warn("option skip_proofs")
-            false
-          }
-          else true
-        }
-      } yield (options, name)
+        } yield entry
+      Graph.make[Document.Node.Name, Options](used, permissive = true)(
+        Document.Node.Name.Theory_Ordering)
     }
 
     def sources(name: String): List[SHA1.Digest] =
@@ -370,6 +373,10 @@
                 theories = dependencies.entries,
                 loaded_files = loaded_files)
 
+            val used_theories =
+              for ((options, name) <- dependencies.adjunct_theories)
+              yield ((name, options), known.theories(name.theory).imports)
+
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
 
@@ -387,7 +394,7 @@
                 doc_names = doc_names,
                 global_theories = global_theories,
                 loaded_theories = dependencies.loaded_theories,
-                used_theories = dependencies.adjunct_theories,
+                used_theories = used_theories,
                 dump_checkpoint = dump_checkpoint,
                 known = known,
                 overall_syntax = overall_syntax,