make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive

--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Dec 16 15:12:17 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Dec 16 15:12:17 2010 +0100
@@ -552,11 +552,14 @@
 
 \opfalse{verbose}{quiet}
 Specifies whether the \textbf{sledgehammer} command should explain what it does.
+This option is implicitly disabled for automatic runs.
 
 \opfalse{debug}{no\_debug}
 Specifies whether Sledgehammer should display additional debugging information
 beyond what \textit{verbose} already displays. Enabling \textit{debug} also
-enables \textit{verbose} behind the scenes.
+enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
+behind the scenes. The \textit{debug} option is implicitly disabled for
+automatic runs.
 
 \nopagebreak
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -75,10 +75,10 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("blocking", "false"),
-   ("debug", "false"),
+  [("debug", "false"),
    ("verbose", "false"),
    ("overlord", "false"),
+   ("blocking", "false"),
    ("type_sys", "smart"),
    ("explicit_apply", "false"),
    ("relevance_thresholds", "0.45 0.85"),
@@ -91,10 +91,10 @@
    ("atps", "provers"), (* FIXME: legacy *)
    ("atp", "provers")]  (* FIXME: legacy *)
 val negated_alias_params =
-  [("non_blocking", "blocking"),
-   ("no_debug", "debug"),
+  [("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
+   ("non_blocking", "blocking"),
    ("partial_types", "full_types"),
    ("implicit_apply", "explicit_apply"),
    ("no_isar_proof", "isar_proof")]
@@ -219,10 +219,10 @@
       case lookup name of
         SOME "smart" => NONE
       | _ => SOME (lookup_int name)
-    val blocking = auto orelse lookup_bool "blocking"
     val debug = not auto andalso lookup_bool "debug"
     val verbose = debug orelse (not auto andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
+    val blocking = auto orelse debug orelse lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
     val type_sys =
@@ -244,7 +244,7 @@
     val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
     val expect = lookup_string "expect"
   in
-    {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
+    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
      relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
      isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -54,7 +54,7 @@
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
     val params =
-      {blocking = true, debug = debug, verbose = false, overlord = overlord,
+      {debug = debug, verbose = false, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -16,10 +16,10 @@
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
 
   type params =
-    {blocking: bool,
-     debug: bool,
+    {debug: bool,
      verbose: bool,
      overlord: bool,
+     blocking: bool,
      provers: string list,
      type_sys: type_system,
      explicit_apply: bool,
@@ -214,10 +214,10 @@
 (** problems, results, ATPs, etc. **)
 
 type params =
-  {blocking: bool,
-   debug: bool,
+  {debug: bool,
    verbose: bool,
    overlord: bool,
+   blocking: bool,
    provers: string list,
    type_sys: type_system,
    explicit_apply: bool,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -26,7 +26,7 @@
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
 
-fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
+fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
                        n goal =
   quote name ^
   (if verbose then
@@ -41,7 +41,7 @@
 
 val implicit_minimization_threshold = 50
 
-fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
+fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
                auto minimize_command only
                {state, goal, subgoal, subgoal_count, facts} name =
   let
@@ -118,7 +118,7 @@
 (* FUDGE *)
 val auto_max_relevant_divisor = 2
 
-fun run_sledgehammer (params as {blocking, debug, provers, type_sys,
+fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
                                  relevance_thresholds, max_relevant, ...})
                      auto i (relevance_override as {only, ...}) minimize_command
                      state =