# HG changeset patch
# User boehmes
# Date 1252164870 -7200
# Node ID ba397aa0ff5d5eefc56052111490e2a5279fc623
# Parent  1b70db55c81145c51522f8be8c3d38d46c1af04d
separate output of ATP user time and sledgehammer (ML code) user time

diff -r 1b70db55c811 -r ba397aa0ff5d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 05 15:46:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 05 17:34:30 2009 +0200
@@ -149,13 +149,13 @@
     val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
     val atp_timeout = AtpManager.get_timeout () 
     val atp = prover atp_timeout NONE NONE prover_name 1
-    val ((success, (message, thm_names), time, _, _, _), time') =
+    val ((success, (message, thm_names), atp_time, _, _, _), sh_time) =
       TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st)
   in
-    if success then (message, SOME (time + time', thm_names))
+    if success then (message, SOME (atp_time, sh_time, thm_names))
     else (message, NONE)
   end
-  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
+  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, 0, []))
        | TimeLimit.TimeOut => ("timeout", NONE)
        | ERROR msg => ("error: " ^ msg, NONE)
 
@@ -170,19 +170,19 @@
     val dir = AList.lookup (op =) args keepK
     val (msg, result) =
       safe init_sh done_sh (run_sh prover_name timeout st) dir
-    val _ =
-      if is_some result
-      then
+  in
+    (case result of
+      SOME (atp_time, sh_time, names) =>
         let
-          val time = fst (the result)
           val _ = change_data id inc_sh_success
-          val _ = change_data id (inc_sh_time time)
+          val _ = change_data id (inc_sh_time (atp_time + sh_time))
+          val _ = change thm_names (K (SOME names))
         in
-          log (sh_tag id ^ "succeeded (" ^ string_of_int time ^ ") [" ^
-            prover_name ^ "]:\n" ^ msg)
+          log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^
+            string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
         end
-      else log (sh_tag id ^ "failed: " ^ msg)
-  in change thm_names (K (Option.map snd result)) end
+    | NONE => log (sh_tag id ^ "failed: " ^ msg))
+  end
 
 end