made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired

--- a/src/Doc/Sledgehammer/document/root.tex	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Feb 20 08:44:24 2013 +0100
@@ -308,7 +308,7 @@
 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
 fast the call is. You can click the proof to insert it into the theory text.
 
-In addition, you can ask Sledgehammer for an Isar text proof by passing the
+In addition, you can ask Sledgehammer for an Isar text proof by enabling the
 \textit{isar\_proofs} option (\S\ref{output-format}):
 
 \prew
@@ -367,7 +367,7 @@
 if that helps.
 
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, instead of one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-liner \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
 \textit{isar\_compress} (\S\ref{output-format}).
 
@@ -501,15 +501,15 @@
 using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
 strongly encouraged to report this to the author at \authoremail.
 
-\point{Why are the generated Isar proofs so ugly/broken?}
-
-The current implementation of the Isar proof feature,
-enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
-is highly experimental. Work on a new implementation has begun. There is a large body of
-research into transforming resolution proofs into natural deduction proofs (such
-as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
-value or to try several provers and keep the nicest-looking proof.
+%\point{Why are the generated Isar proofs so ugly/broken?}
+%
+%The current implementation of the Isar proof feature,
+%enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
+%is experimental. Work on a new implementation has begun. There is a large body of
+%research into transforming resolution proofs into natural deduction proofs (such
+%as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
+%set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
+%value or to try several provers and keep the nicest-looking proof.
 
 \point{How can I tell whether a suggested proof is sound?}
 
@@ -1296,16 +1296,18 @@
 \nopagebreak
 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
 
-\opfalse{isar\_proofs}{no\_isar\_proofs}
+\opsmart{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. Isar proof construction is still experimental and often
-fails; however, they are usually faster and sometimes more robust than
-\textit{metis} proofs.
+\textit{metis} proofs. The construction of Isar proof is still experimental and
+may sometimes fail; however, when they succeed they are usually faster and more
+intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
+(the default), Isar proofs are only generated when no working one-liner
+\textit{metis} proof is available.
 
 \opdefault{isar\_compress}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
-is enabled. A value of $n$ indicates that each Isar proof step should correspond
-to a group of up to $n$ consecutive proof steps in the ATP proof.
+is explicitly enabled. A value of $n$ indicates that each Isar proof step should
+correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
 
 \optrueonly{dont\_compress\_isar}
 Alias for ``\textit{isar\_compress} = 0''.

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -94,7 +94,7 @@
    ("fact_thresholds", "0.45 0.85"),
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
-   ("isar_proofs", "false"),
+   ("isar_proofs", "smart"),
    ("isar_compress", "10"),
    ("slice", "true"),
    ("minimize", "smart"),
@@ -313,7 +313,7 @@
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
-    val isar_proofs = lookup_bool "isar_proofs"
+    val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val isar_compress = Real.max (1.0, lookup_real "isar_compress")
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -293,24 +293,21 @@
                 <= Config.get ctxt auto_minimize_max_time
               fun prover_fast_enough () = can_min_fast_enough run_time
             in
-              if isar_proofs then
-                ((prover_fast_enough (), (name, params)), preplay)
-              else
-                (case Lazy.force preplay of
-                   Played (reconstr as Metis _, timeout) =>
-                   if can_min_fast_enough timeout then
-                     (true, extract_reconstructor params reconstr
-                            ||> (fn override_params =>
-                                    adjust_reconstructor_params
-                                        override_params params))
-                   else
-                     (prover_fast_enough (), (name, params))
-                 | Played (SMT, timeout) =>
-                   (* Cheat: assume the original prover is as fast as "smt" for
-                      the goal it proved itself *)
-                   (can_min_fast_enough timeout, (name, params))
-                 | _ => (prover_fast_enough (), (name, params)),
-                 preplay)
+              (case Lazy.force preplay of
+                 Played (reconstr as Metis _, timeout) =>
+                 if can_min_fast_enough timeout then
+                   (true, extract_reconstructor params reconstr
+                          ||> (fn override_params =>
+                                  adjust_reconstructor_params override_params
+                                      params))
+                 else
+                   (prover_fast_enough (), (name, params))
+               | Played (SMT, timeout) =>
+                 (* Cheat: assume the original prover is as fast as "smt" for
+                    the goal it proved itself *)
+                 (can_min_fast_enough timeout, (name, params))
+               | _ => (prover_fast_enough (), (name, params)),
+               preplay)
             end
         else
           ((false, (name, params)), preplay)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -34,7 +34,7 @@
      fact_thresholds : real * real,
      max_mono_iters : int option,
      max_new_mono_instances : int option,
-     isar_proofs : bool,
+     isar_proofs : bool option,
      isar_compress : real,
      slice : bool,
      minimize : bool option,
@@ -323,7 +323,7 @@
    fact_thresholds : real * real,
    max_mono_iters : int option,
    max_new_mono_instances : int option,
-   isar_proofs : bool,
+   isar_proofs : bool option,
    isar_compress : real,
    slice : bool,
    minimize : bool option,
@@ -795,7 +795,7 @@
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
-            val full_proof = debug orelse isar_proofs
+            val full_proof = debug orelse isar_proofs = SOME true
             val args =
               arguments ctxt full_proof extra
                         (slice_timeout |> the_default one_day)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -38,9 +38,10 @@
     string list option
   val one_line_proof_text : int -> one_line_params -> string
   val isar_proof_text :
-    Proof.context -> bool -> isar_params -> one_line_params -> string
+    Proof.context -> bool option -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool -> isar_params -> int -> one_line_params -> string
+    Proof.context -> bool option -> isar_params -> int -> one_line_params
+    -> string
 end;
 
 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -831,7 +832,7 @@
               else
                 compress_proof debug ctxt type_enc lam_trans preplay
                   preplay_timeout
-                  (if isar_proofs then isar_compress else 1000.0))
+                  (if isar_proofs = SOME true then isar_compress else 1000.0))
           |>> cleanup_labels_in_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
@@ -839,7 +840,7 @@
       in
         case isar_text of
           "" =>
-          if isar_proofs then
+          if isar_proofs = SOME true then
             "\nNo structured proof available (proof too simple)."
           else
             ""
@@ -870,7 +871,7 @@
         isar_proof_of ()
       else case try isar_proof_of () of
         SOME s => s
-      | NONE => if isar_proofs then
+      | NONE => if isar_proofs = SOME true then
                   "\nWarning: The Isar proof construction failed."
                 else
                   ""
@@ -884,7 +885,8 @@
 
 fun proof_text ctxt isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
-  (if isar_proofs orelse isar_proof_would_be_a_good_idea preplay then
+  (if isar_proofs = SOME true orelse
+      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
      isar_proof_text ctxt isar_proofs isar_params
    else
      one_line_proof_text num_chained) one_line_params