proper error;
authorwenzelm
Sun, 01 Jul 2018 12:37:24 +0200
changeset 68557 5a836f1b588c
parent 68552 391e89e03eef
child 68558 7aae213d9e69
proper error;
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)
+    }
   }