# HG changeset patch
# User wenzelm
# Date 1527610148 -7200
# Node ID 1d33697199c1c215b273189adbaa49fcd91da0b4
# Parent  2e168460a9c31de2020901a331128e1538d7e1c9
shutdown ML process before output: Theories_Result is timeless/stateless;

diff -r 2e168460a9c3 -r 1d33697199c1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue May 29 17:45:48 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Tue May 29 18:09:08 2018 +0200
@@ -100,13 +100,16 @@
       Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
         include_sessions = include_sessions, progress = progress, log = log)
 
-    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()
+    val theories_result = session.use_theories(use_theories, progress = progress)
+    val session_result = session.stop()
+
+
+    /* dump aspects */
+
+    val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+    aspects.foreach(_.operation(aspect_args))
+
+    session_result
   }