# HG changeset patch
# User wenzelm
# Date 1527599042 -7200
# Node ID 5971199863eaab75efd6898fa2ff747b187ae370
# Parent  938803796a8b317449a24fa36e59a37b14e38c70
more accurate dependencies;
tuned;

diff -r 938803796a8b -r 5971199863ea src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue May 29 14:45:54 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue May 29 15:04:02 2018 +0200
@@ -146,6 +146,7 @@
     doc_names: List[String] = Nil,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
+    used_theories: List[Document.Node.Name] = Nil,
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -349,6 +350,7 @@
                 doc_names = doc_names,
                 global_theories = global_theories,
                 loaded_theories = dependencies.loaded_theories,
+                used_theories = dependencies.theories,
                 known = known,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
diff -r 938803796a8b -r 5971199863ea src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue May 29 14:45:54 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Tue May 29 15:04:02 2018 +0200
@@ -50,21 +50,32 @@
 
     val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
 
+
+    /* dependencies */
+
     val deps =
       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
         selection_deps(selection)
 
+    val include_sessions =
+      deps.sessions_structure.imports_topological_order
+
+    val use_theories =
+      deps.sessions_structure.build_topological_order.
+        flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
+
+
+    /* session */
+
     val session =
       Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
-        include_sessions = deps.sessions_structure.imports_topological_order,
-        progress = progress, log = log)
+        include_sessions = include_sessions, progress = progress, log = log)
 
-    val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
-    val theories_result = session.use_theories(theories, progress = progress)
-
-    val args = Aspect_Args(dump_options, progress, output_dir, theories_result)
-
-    try { aspects.foreach(aspect => aspect.operation(args)) }
+    try {
+      val theories_result = session.use_theories(use_theories, progress = progress)
+      val args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+      aspects.foreach(_.operation(args))
+    }
     catch { case exn: Throwable => session.stop (); throw exn }
     session.stop()
   }