# HG changeset patch
# User blanchet
# Date 1292703874 -3600
# Node ID 6a9306c427b93b5549ab93cf4437b7c7412e4d44
# Parent  35ce17cd796735282ce8a89c286e61f695808113
handle timeouts in Mirabelle more gracefully

diff -r 35ce17cd7967 -r 6a9306c427b9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 21:07:34 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 21:24:34 2010 +0100
@@ -382,10 +382,13 @@
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
-    val ({outcome, message, used_facts, run_time_in_msecs, ...}
+    val ({outcome, message, used_facts, run_time_in_msecs}
          : Sledgehammer_Provers.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
                       (prover params (K ""))) problem
+      handle TimeLimit.TimeOut =>
+             ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
+               run_time_in_msecs = NONE}, ~1)
     val time_prover = run_time_in_msecs |> the_default ~1
   in
     case outcome of
@@ -393,7 +396,6 @@
     | SOME _ => (message, SH_FAIL (time_isa, time_prover))
   end
   handle ERROR msg => ("error: " ^ msg, SH_ERROR)
-       | TimeLimit.TimeOut => ("timeout", SH_ERROR)
 
 fun thms_of_name ctxt name =
   let