make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
authorblanchet
Wed, 15 Dec 2010 19:41:24 +0100
changeset 41180 a99bc6f3664b
parent 41179 5391d34b0f4c
child 41181 9240be8c8c69
make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 18:45:14 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 19:41:24 2010 +0100
@@ -193,6 +193,7 @@
         run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
+        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
     in
       (false, state)
       |> (if blocking then run_atps #> not auto ? run_smts