added "blocking" option to Sledgehammer to run in synchronous mode;
sometimes useful, e.g. for testing

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 22:27:33 2010 +0200
@@ -13,7 +13,8 @@
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
   type params =
-    {debug: bool,
+    {blocking: bool,
+     debug: bool,
      verbose: bool,
      overlord: bool,
      atps: string list,
@@ -80,7 +81,8 @@
 (** problems, results, provers, etc. **)
 
 type params =
-  {debug: bool,
+  {blocking: bool,
+   debug: bool,
    verbose: bool,
    overlord: bool,
    atps: string list,
@@ -362,8 +364,9 @@
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
-                        relevance_override minimize_command proof_state
+fun start_prover_thread (params as {blocking, verbose, full_types, timeout,
+                                    ...})
+                        i n relevance_override minimize_command proof_state
                         atp_name =
   let
     val thy = Proof.theory_of proof_state
@@ -374,23 +377,25 @@
     val desc =
       "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
+    fun run () =
+      let
+        val problem =
+          {subgoal = i, goal = (ctxt, (facts, goal)),
+           relevance_override = relevance_override, axioms = NONE}
+      in
+        prover params (minimize_command atp_name) problem |> #message
+        handle ERROR message => "Error: " ^ message ^ "\n"
+             | exn => "Internal error:\n" ^ ML_Compiler.exn_message exn ^ "\n"
+      end
   in
-    Async_Manager.launch das_Tool verbose birth_time death_time desc
-        (fn () =>
-            let
-              val problem =
-                {subgoal = i, goal = (ctxt, (facts, goal)),
-                 relevance_override = relevance_override, axioms = NONE}
-            in
-              prover params (minimize_command atp_name) problem |> #message
-              handle ERROR message => "Error: " ^ message ^ "\n"
-                   | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
-                            "\n"
-            end)
+    if blocking then
+      priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
+    else
+      Async_Manager.launch das_Tool verbose birth_time death_time desc run
   end
 
 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
-  | run_sledgehammer (params as {atps, ...}) i relevance_override
+  | run_sledgehammer (params as {blocking, atps, ...}) i relevance_override
                      minimize_command state =
     case subgoal_count state of
       0 => priority "No subgoal!"
@@ -398,8 +403,10 @@
       let
         val _ = kill_atps ()
         val _ = priority "Sledgehammering..."
-        val _ = app (start_prover_thread params i n relevance_override
-                                         minimize_command state) atps
+        val _ =
+          (if blocking then Par_List.map else map)
+              (start_prover_thread params i n relevance_override
+                                   minimize_command state) atps
       in () end
 
 val setup =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 31 22:27:33 2010 +0200
@@ -49,8 +49,8 @@
     val _ =
       priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
     val params =
-      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
-       full_types = full_types, explicit_apply = explicit_apply,
+      {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
+       atps = atps, full_types = full_types, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        theory_relevant = NONE, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, timeout = timeout}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 22:27:33 2010 +0200
@@ -63,7 +63,8 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("debug", "false"),
+  [("blocking", "false"),
+   ("debug", "false"),
    ("verbose", "false"),
    ("overlord", "false"),
    ("explicit_apply", "false"),
@@ -76,7 +77,8 @@
 val alias_params =
   [("atp", "atps")]
 val negated_alias_params =
-  [("no_debug", "debug"),
+  [("non_blocking", "blocking"),
+   ("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("partial_types", "full_types"),
@@ -167,6 +169,7 @@
       case lookup name of
         SOME "smart" => NONE
       | _ => SOME (lookup_int name)
+    val blocking = lookup_bool "blocking"
     val debug = lookup_bool "debug"
     val verbose = debug orelse lookup_bool "verbose"
     val overlord = lookup_bool "overlord"
@@ -182,8 +185,8 @@
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val timeout = lookup_time "timeout"
   in
-    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
-     full_types = full_types, explicit_apply = explicit_apply,
+    {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
+     atps = atps, full_types = full_types, explicit_apply = explicit_apply,
      relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
      theory_relevant = theory_relevant, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, timeout = timeout}