# HG changeset patch
# User wenzelm
# Date 1530441444 -7200
# Node ID 5a836f1b588c7e75854a1ff23e7a4879065cea9d
# Parent  391e89e03eef99743610d82b7e88051ac58e974e
proper error;

diff -r 391e89e03eef -r 5a836f1b588c src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Jun 30 18:58:13 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sun Jul 01 12:37:24 2018 +0200
@@ -132,7 +132,15 @@
       aspects.foreach(_.operation(aspect_args))
     }
 
-    session_result
+    if (theories_result.ok) session_result
+    else {
+      for {
+        (name, status) <- theories_result.nodes if !status.ok
+        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
+      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
+
+      session_result.copy(rc = session_result.rc max 1)
+    }
   }