# HG changeset patch
# User blanchet
# Date 1391190196 -3600
# Node ID a4ef6eb1fc20fa603dcb8ac9b843249dfa9b9e46
# Parent  ee90eebb8b735b834b5570f203e51decf4a7f3a9
added a 'trace' option

diff -r ee90eebb8b73 -r a4ef6eb1fc20 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
@@ -13,6 +13,8 @@
   type stature = ATP_Problem_Generate.stature
   type one_line_params = Sledgehammer_Reconstructor.one_line_params
 
+  val trace : bool Config.T
+
   type isar_params =
     bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
 
@@ -42,6 +44,8 @@
 
 open String_Redirect
 
+val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
+
 val e_skolemize_rules = ["skolemize", "shift_quantors"]
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
@@ -262,7 +266,7 @@
         val string_of_isar_proof =
           string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
 
-        val trace = false
+        val trace = Config.get ctxt trace
 
         val isar_proof =
           refute_graph
@@ -273,13 +277,17 @@
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
-        val preplay_data as {overall_preplay_outcome, ...} =
+        val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
           preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
             preplay_timeout isar_proof
 
+        fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
+        fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
+
         fun trace_isar_proof label proof =
           if trace then
-            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof true proof ^ "\n")
+            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
+              "\n")
           else
             ()
 
@@ -299,7 +307,7 @@
           ||> kill_useless_labels_in_isar_proof
           ||> relabel_isar_proof_finally
       in
-        (case string_of_isar_proof false isar_proof of
+        (case string_of_isar_proof (K (K "")) isar_proof of
           "" =>
           if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
           else ""
diff -r ee90eebb8b73 -r a4ef6eb1fc20 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
@@ -30,6 +30,8 @@
   val label_ord : label * label -> order
   val string_of_label : label -> string
 
+  val string_of_proof_method : proof_method -> string
+
   val steps_of_proof : isar_proof -> isar_step list
 
   val label_of_step : isar_step -> label option
@@ -48,8 +50,8 @@
   val relabel_isar_proof_canonically : isar_proof -> isar_proof
   val relabel_isar_proof_finally : isar_proof -> isar_proof
 
-  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> bool ->
-    isar_proof -> string
+  val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
+    (label -> proof_method list list -> string) -> isar_proof -> string
 end;
 
 structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -86,7 +88,7 @@
 
 fun string_of_label (s, num) = s ^ string_of_int num
 
-fun string_of_method meth =
+fun string_of_proof_method meth =
   (case meth of
     Metis_Method => "metis"
   | Simp_Method => "simp"
@@ -242,7 +244,7 @@
 
 val indent_size = 2
 
-fun string_of_isar_proof ctxt type_enc lam_trans i n all_methods proof =
+fun string_of_isar_proof ctxt type_enc lam_trans i n comment_of proof =
   let
     (* Make sure only type constraints inserted by the type annotation code are printed. *)
     val ctxt =
@@ -295,9 +297,7 @@
     fun of_method ls ss Metis_Method =
         using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
       | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
-      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_method meth
-
-    val str_of_methodss = map (map string_of_method) #> map commas #> space_implode "; "
+      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_proof_method meth
 
     fun of_free (s, T) =
       maybe_quote s ^ " :: " ^
@@ -340,7 +340,7 @@
         add_str (of_indent ind ^ "let ")
         #> add_term t1 #> add_str " = " #> add_term t2
         #> add_str "\n"
-      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: meths) :: methss))) =
+      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (meth :: _) :: _))) =
         add_step_pre ind qs subproofs
         #> (case xs of
              [] => add_str (of_have qs (length subproofs) ^ " ")
@@ -350,8 +350,9 @@
         #> add_term t
         #> add_str (" " ^
              of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
-             (if all_methods then " (* " ^ str_of_methodss (meths :: methss) ^ " *)" else "") ^
-             "\n")
+             (case comment_of l methss of
+               "" => ""
+             | comment => " (* " ^ comment ^ " *)") ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
       ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst