# HG changeset patch
# User wenzelm
# Date 1571071872 -7200
# Node ID f5d0aebfd89c164f0be93791f8eb21e2cd2038c7
# Parent  6e6254bbce1f40ddcb9d8f591750196e5dc9d1f1
proper guard -- avoid bad result;

diff -r 6e6254bbce1f -r f5d0aebfd89c src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 17:19:08 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 18:51:12 2019 +0200
@@ -239,26 +239,28 @@
               {
                 val (snapshot, status) = args
                 val name = snapshot.node_name
-                if (status.ok && selected_theory(name)) {
-                  try { process_theory(Args(session, snapshot, status)) }
-                  catch {
-                    case exn: Throwable if !Exn.is_interrupt(exn) =>
-                      val msg = Exn.message(exn)
-                      progress.echo("FAILED to process theory " + name)
-                      progress.echo_error_message(msg)
-                      consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
+                if (selected_theory(name)) {
+                  if (status.ok) {
+                    try { process_theory(Args(session, snapshot, status)) }
+                    catch {
+                      case exn: Throwable if !Exn.is_interrupt(exn) =>
+                        val msg = Exn.message(exn)
+                        progress.echo("FAILED to process theory " + name)
+                        progress.echo_error_message(msg)
+                        consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
+                    }
                   }
-                }
-                else {
-                  val msgs =
-                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
-                    yield {
-                      "Error" + Position.here(pos) + ":\n" +
-                        XML.content(Pretty.formatted(List(tree)))
-                    }
-                  progress.echo("FAILED to process theory " + name)
-                  msgs.foreach(progress.echo_error_message)
-                  consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
+                  else {
+                    val msgs =
+                      for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
+                      yield {
+                        "Error" + Position.here(pos) + ":\n" +
+                          XML.content(Pretty.formatted(List(tree)))
+                      }
+                    progress.echo("FAILED to process theory " + name)
+                    msgs.foreach(progress.echo_error_message)
+                    consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
+                  }
                 }
                 true
               })