src/Pure/Tools/dump.scala
changeset 68557 5a836f1b588c
parent 68537 0299c1dccc96
child 68741 e90cf766723c
child 68743 91162dd89571
     1.1 --- a/src/Pure/Tools/dump.scala	Sat Jun 30 18:58:13 2018 +0100
     1.2 +++ b/src/Pure/Tools/dump.scala	Sun Jul 01 12:37:24 2018 +0200
     1.3 @@ -132,7 +132,15 @@
     1.4        aspects.foreach(_.operation(aspect_args))
     1.5      }
     1.6  
     1.7 -    session_result
     1.8 +    if (theories_result.ok) session_result
     1.9 +    else {
    1.10 +      for {
    1.11 +        (name, status) <- theories_result.nodes if !status.ok
    1.12 +        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
    1.13 +      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
    1.14 +
    1.15 +      session_result.copy(rc = session_result.rc max 1)
    1.16 +    }
    1.17    }
    1.18  
    1.19