--- 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()
}