merged

--- a/src/Pure/Tools/build.scala	Sat Dec 29 18:21:13 2018 +0000
+++ b/src/Pure/Tools/build.scala	Sat Dec 29 18:40:29 2018 +0000
@@ -844,14 +844,18 @@
     progress: Progress = No_Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
-    system_mode: Boolean = false): Int =
+    system_mode: Boolean = false,
+    strict: Boolean = false): Int =
   {
-    if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
-        system_mode = system_mode, sessions = List(logic)).ok) 0
-    else {
-      progress.echo("Build started for Isabelle/" + logic + " ...")
-      Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
-        system_mode = system_mode, sessions = List(logic)).rc
-    }
+    val rc =
+      if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
+          system_mode = system_mode, sessions = List(logic)).ok) 0
+      else {
+        progress.echo("Build started for Isabelle/" + logic + " ...")
+        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+          system_mode = system_mode, sessions = List(logic)).rc
+      }
+
+    if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }

--- a/src/Pure/Tools/dump.scala	Sat Dec 29 18:21:13 2018 +0000
+++ b/src/Pure/Tools/dump.scala	Sat Dec 29 18:40:29 2018 +0000
@@ -212,8 +212,8 @@
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
-    if (Build.build_logic(options, logic, build_heap = true, progress = progress,
-      dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
+    Build.build_logic(options, logic, build_heap = true, progress = progress,
+      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
 
     val dump_options = make_options(options, aspects)