# HG changeset patch
# User wenzelm
# Date 1537615363 -7200
# Node ID 90bb4cabe1e870ef55d58dd8f86d04afaeb3fda0
# Parent  30e88eabf1670807aed63e8f0083b97854863a4d
clarified errors: no result from forced session.stop, check pending theories;

diff -r 30e88eabf167 -r 90bb4cabe1e8 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Sep 21 23:14:52 2018 +0100
+++ b/src/Pure/PIDE/headless.scala	Sat Sep 22 13:22:43 2018 +0200
@@ -71,6 +71,12 @@
     val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
     val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
   {
+    def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
+    {
+      val committed = nodes_committed.iterator.map(_._1).toSet
+      nodes.filter(p => !committed(p._1))
+    }
+
     def snapshot(name: Document.Node.Name): Document.Snapshot =
       stable_snapshot(state, version, name)
 
diff -r 30e88eabf167 -r 90bb4cabe1e8 src/Pure/Tools/dump.scala
--- 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)
     })
 }