# HG changeset patch
# User wenzelm
# Date 1536341248 -7200
# Node ID 19ddfe546620d228ffe47aa252fa5222b79a147d
# Parent  10cbb5d9908159b2823e3d5309a8ec454340bf4f
clarified error progress and error_rc;

diff -r 10cbb5d99081 -r 19ddfe546620 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Sep 07 19:18:41 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Sep 07 19:27:28 2018 +0200
@@ -118,7 +118,7 @@
 
     object Consumer
     {
-      private val errors = Synchronized[List[String]](Nil)
+      private val consumer_ok = Synchronized(true)
 
       private val consumer =
         Consumer_Thread.fork(name = "dump")(
@@ -130,9 +130,12 @@
                   Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
                 aspects.foreach(_.operation(aspect_args))
               }
-              for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
-                val msg = XML.content(Pretty.formatted(List(tree)))
-                errors.change(("Error" + Position.here(pos) + ":\n" + msg) :: _)
+              else {
+                consumer_ok.change(_ => false)
+                for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
+                  val msg = XML.content(Pretty.formatted(List(tree)))
+                  progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg)
+                }
               }
               true
             })
@@ -140,10 +143,10 @@
       def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
         consumer.send((snapshot, node_status))
 
-      def shutdown(): List[String] =
+      def shutdown(): Boolean =
       {
         consumer.shutdown()
-        errors.value.reverse
+        consumer_ok.value
       }
     }
 
@@ -159,9 +162,10 @@
 
     val session_result = session.stop()
 
-    Consumer.shutdown().foreach(progress.echo_error_message(_))
+    val consumer_ok = Consumer.shutdown()
 
-    if (theories_result.ok) session_result else session_result.error_rc
+    if (theories_result.ok && consumer_ok) session_result
+    else session_result.error_rc
   }