shutdown ML process before output: Theories_Result is timeless/stateless;

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