make output more concise

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
@@ -248,9 +248,7 @@
   | minimize_line minimize_command ss =
     case minimize_command ss of
       "" => ""
-    | command =>
-      "\nTo minimize the number of lemmas, try this: " ^
-      Markup.markup Markup.sendback command ^ "."
+    | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
 
 val split_used_facts =
   List.partition (curry (op =) Chained o snd)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
@@ -318,8 +318,10 @@
   |> Exn.release
   |> tap (after path)
 
-fun proof_banner auto =
-  if auto then "Auto Sledgehammer found a proof" else "Try this command"
+fun proof_banner auto blocking name =
+  if auto then "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
+  else if blocking then quote name ^ " found a proof"
+  else "Try this command"
 
 val smt_triggers =
   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -472,8 +474,8 @@
 fun run_atp auto name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
-        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
-          max_new_mono_instances, explicit_apply, isar_proof,
+        ({debug, verbose, overlord, blocking, type_sys, max_relevant,
+          max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
           isar_shrink_factor, slicing, timeout, ...} : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
@@ -711,8 +713,8 @@
     val isar_params =
       (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
     val metis_params =
-      (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
-       fact_names, typed_helpers, goal, subgoal)
+      (proof_banner auto blocking name, minimize_command, type_sys, atp_proof,
+       facts_offset, fact_names, typed_helpers, goal, subgoal)
     val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>
@@ -884,7 +886,8 @@
             (Config.put Metis_Tactics.verbose debug
              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
-fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
+fun run_smt_solver auto name (params as {debug, verbose, blocking, ...})
+                   minimize_command
                    ({state, subgoal, subgoal_count, facts, smt_filter, ...}
                     : prover_problem) =
   let
@@ -907,7 +910,7 @@
               ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
                       else "smt_solver = " ^ maybe_quote name)
         in
-          try_command_line (proof_banner auto)
+          try_command_line (proof_banner auto blocking name)
               (apply_on_subgoal settings subgoal subgoal_count ^
                command_call method (map fst other_lemmas)) ^
           minimize_line minimize_command

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:07 2011 +0200
@@ -104,7 +104,7 @@
       max_relevant
       |> the_default (default_max_relevant_for_prover ctxt slicing name)
     val num_facts = length facts |> not only ? Integer.min max_relevant
-    val desc =
+    fun desc () =
       prover_description ctxt params name num_facts subgoal subgoal_count goal
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
@@ -145,25 +145,28 @@
       in (outcome_code, message) end
   in
     if auto then
-      let
-        val (outcome_code, message) = TimeLimit.timeLimit timeout go ()
-        val success = (outcome_code = someN)
-      in
-        (success, state |> success ? Proof.goal_message (fn () =>
-             Pretty.chunks [Pretty.str "",
-                            Pretty.mark Markup.hilite (Pretty.str message)]))
+      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+        (outcome_code,
+         state
+         |> outcome_code = someN
+            ? Proof.goal_message (fn () =>
+                  [Pretty.str "",
+                   Pretty.mark Markup.hilite (Pretty.str message)]
+                  |> Pretty.chunks))
       end
     else if blocking then
-      let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in
-        Async_Manager.implode_desc desc ^ "\n" ^ message
+      let
+        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
+      in
+        (if outcome_code = someN then message else quote name ^ ": " ^ message)
         |> Async_Manager.break_into_chunks
         |> List.app Output.urgent_message;
-        (outcome_code = someN, state)
+        (outcome_code, state)
       end
     else
-      (Async_Manager.launch das_tool birth_time death_time desc
+      (Async_Manager.launch das_tool birth_time death_time (desc ())
                             (apfst (curry (op <>) timeoutN) o go);
-       (false, state))
+       (unknownN, state))
   end
 
 fun class_of_smt_solver ctxt name =
@@ -216,7 +219,9 @@
              facts = facts,
              smt_filter = maybe_smt_filter
                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
-          val launch = launch_prover params auto minimize_command only
+          fun launch problem =
+            launch_prover params auto minimize_command only problem
+            #>> curry (op =) someN
         in
           if auto then
             fold (fn prover => fn (true, state) => (true, state)