more explicit sendback propertries based on mode;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Sat Aug 17 11:34:50 2013 +0200
@@ -13,7 +13,7 @@
 
   val string_of_reconstructor : reconstructor -> string
 
-  val one_line_proof_text : bool -> int -> one_line_params -> string
+  val one_line_proof_text : Properties.T -> int -> one_line_params -> string
 
   val string_of_proof :
     Proof.context -> string -> string -> int -> int -> isar_proof -> string
@@ -71,25 +71,23 @@
   using_labels ls ^ apply_on_subgoal i n ^
   command_call (string_of_reconstructor reconstr) ss
 
-fun try_command_line auto banner time command =
+fun try_command_line sendback_props banner time command =
   banner ^ ": " ^
-  Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^
+  Active.sendback_markup sendback_props command ^
   show_time time ^ "."
 
 fun minimize_line _ _ [] = ""
-  | minimize_line auto minimize_command ss =
+  | minimize_line sendback_props minimize_command ss =
     case minimize_command ss of
       "" => ""
     | command =>
-      "\nTo minimize: " ^
-      Active.sendback_markup (if auto then [Markup.padding_command] else [])
-                             command ^ "."
+      "\nTo minimize: " ^ Active.sendback_markup sendback_props command ^ "."
 
 fun split_used_facts facts =
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
         |> pairself (sort_distinct (string_ord o pairself fst))
 
-fun one_line_proof_text auto num_chained
+fun one_line_proof_text sendback_props num_chained
         (preplay, banner, used_facts, minimize_command, subgoal,
          subgoal_count) =
   let
@@ -113,8 +111,8 @@
                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
                      \solve this.)"
           else
-            try_command_line auto banner ext_time)
-  in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end
+            try_command_line sendback_props banner ext_time)
+  in try_line ^ minimize_line sendback_props minimize_command (map fst (extra @ chained)) end
 
 
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Aug 17 11:34:50 2013 +0200
@@ -464,6 +464,11 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this"
 
+fun sendback_properties mode =
+  if mode = Auto_Try orelse mode = Normal_Result
+  then [Markup.padding_command]
+  else []
+
 fun bunch_of_reconstructors needs_full_types lam_trans =
   if needs_full_types then
     [Metis (full_type_enc, lam_trans false),
@@ -696,6 +701,7 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
+    val sendback_props = sendback_properties mode
     val atp_mode =
       if Config.get ctxt completish then Sledgehammer_Completish
       else Sledgehammer
@@ -976,7 +982,7 @@
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params
+                proof_text ctxt sendback_props isar_proofs isar_params
                            num_chained one_line_params
               end,
            (if verbose then
@@ -1154,6 +1160,7 @@
         ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
+    val sendback_props = sendback_properties mode
     fun weight_facts facts =
       let val num_facts = length facts in
         facts ~~ (0 upto num_facts - 1)
@@ -1181,7 +1188,7 @@
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
-              one_line_proof_text (mode = Auto_Try) num_chained one_line_params
+              one_line_proof_text sendback_props num_chained one_line_params
             end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
@@ -1202,6 +1209,7 @@
         ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
          : prover_problem) =
   let
+    val sendback_props = sendback_properties mode
     val reconstr =
       if name = metisN then
         Metis (type_enc |> the_default (hd partial_type_encs),
@@ -1228,7 +1236,7 @@
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in
-              one_line_proof_text (mode = Auto_Try) num_chained one_line_params
+              one_line_proof_text sendback_props num_chained one_line_params
             end,
        message_tail = ""}
     | play =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Aug 17 11:34:50 2013 +0200
@@ -25,9 +25,9 @@
     Proof.context -> (string * stature) list vector -> 'a proof ->
     string list option
   val isar_proof_text :
-    Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
+    Proof.context -> Properties.T -> bool option -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
+    Proof.context -> Properties.T -> bool option -> isar_params -> int -> one_line_params
     -> string
 end;
 
@@ -412,7 +412,7 @@
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
-fun isar_proof_text ctxt auto isar_proofs
+fun isar_proof_text ctxt sendback_props isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
      isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
      fact_names, lifted, sym_tab, atp_proof, goal)
@@ -425,7 +425,7 @@
       |> (fn fixes =>
              ctxt |> Variable.set_body false
                   |> Proof_Context.add_fixes fixes)
-    val one_line_proof = one_line_proof_text auto 0 one_line_params
+    val one_line_proof = one_line_proof_text sendback_props 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
@@ -625,7 +625,7 @@
             "\n\nStructured proof"
               ^ (commas msg |> not (null msg) ? enclose " (" ")")
               ^ ":\n" ^
-              Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
+              Active.sendback_markup sendback_props isar_text
           end
       end
     val isar_proof =
@@ -645,12 +645,12 @@
   | Trust_Playable _ => true
   | Failed_to_Play _ => true
 
-fun proof_text ctxt auto isar_proofs isar_params num_chained
+fun proof_text ctxt sendback_props isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
-     isar_proof_text ctxt auto isar_proofs isar_params
+     isar_proof_text ctxt sendback_props isar_proofs isar_params
    else
-     one_line_proof_text auto num_chained) one_line_params
+     one_line_proof_text sendback_props num_chained) one_line_params
 
 end;