--- a/src/Pure/Tools/dump.scala Fri Sep 21 23:14:52 2018 +0100
+++ b/src/Pure/Tools/dump.scala Sat Sep 22 13:22:43 2018 +0200
@@ -95,7 +95,7 @@
commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
watchdog_timeout: Time = Headless.default_watchdog_timeout,
system_mode: Boolean = false,
- selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
+ selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
{
if (Build.build_logic(options, logic, build_heap = true, progress = progress,
dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
@@ -167,12 +167,16 @@
commit_cleanup_delay = commit_cleanup_delay,
watchdog_timeout = watchdog_timeout)
- val session_result = session.stop()
+ session.stop()
val consumer_ok = Consumer.shutdown()
- if (use_theories_result.ok && consumer_ok) session_result
- else session_result.error_rc
+ use_theories_result.nodes_pending match {
+ case Nil =>
+ case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
+ }
+
+ use_theories_result.ok && consumer_ok
}
@@ -245,7 +249,7 @@
val progress = new Console_Progress(verbose = verbose)
- val result =
+ val ok =
progress.interrupt_handler {
dump(options, logic,
aspects = aspects,
@@ -266,8 +270,6 @@
sessions = sessions))
}
- progress.echo(result.timing.message_resources)
-
- sys.exit(result.rc)
+ if (!ok) sys.exit(1)
})
}