# HG changeset patch
# User blanchet
# Date 1283377291 -7200
# Node ID aae6a0d33c665f96a34f4e0758ae678b06f66611
# Parent  a02cb5717677c16cfd108e67146e89829e7d97a5
speed up SPASS hack + output time information in "blocking" mode

diff -r a02cb5717677 -r aae6a0d33c66 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:40:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:41:31 2010 +0200
@@ -176,8 +176,9 @@
   |-- Scan.repeat parse_clause_formula_pair
 val extract_clause_formula_relation =
   Substring.full #> Substring.position set_ClauseFormulaRelationN
-  #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
-  #> explode #> parse_clause_formula_relation #> fst
+  #> snd #> Substring.position "." #> fst #> Substring.string
+  #> explode #> filter_out (curry (op =) " ") #> parse_clause_formula_relation
+  #> fst
 
 (* TODO: move to "Sledgehammer_Reconstruct" *)
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
@@ -345,8 +346,7 @@
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-fun start_prover_thread (params as {blocking, verbose, full_types, timeout,
-                                    expect, ...})
+fun start_prover_thread (params as {blocking, timeout, expect, ...})
                         i n relevance_override minimize_command axioms state
                         (prover, atp_name) =
   let
@@ -382,7 +382,7 @@
       end
   in
     if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
-    else Async_Manager.launch das_Tool verbose birth_time death_time desc run
+    else Async_Manager.launch das_Tool birth_time death_time desc run
   end
 
 fun run_sledgehammer (params as {blocking, verbose, atps, full_types,
@@ -393,6 +393,7 @@
       0 => priority "No subgoal!"
     | n =>
       let
+        val timer = Timer.startRealTimer ()
         val _ = () |> not blocking ? kill_atps
         val _ = priority "Sledgehammering..."
         fun run () =
@@ -420,7 +421,14 @@
               (if blocking then Par_List.map else map)
                   (start_prover_thread params i n relevance_override
                                        minimize_command axioms state) provers
-          in () end
+          in
+            if verbose andalso blocking then
+              priority ("Total time: " ^
+                        signed_string_of_int (Time.toMilliseconds
+                            (Timer.checkRealTimer timer)) ^ " ms.")
+            else
+              ()
+          end
       in if blocking then run () else Toplevel.thread true (tap run) |> K () end
 
 val setup =