1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -13,6 +13,8 @@
     1.4    type stature = ATP_Problem_Generate.stature
     1.5    type one_line_params = Sledgehammer_Reconstructor.one_line_params
     1.6  
     1.7 +  val trace : bool Config.T
     1.8 +
     1.9    type isar_params =
    1.10      bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
    1.11  
    1.12 @@ -42,6 +44,8 @@
    1.13  
    1.14  open String_Redirect
    1.15  
    1.16 +val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
    1.17 +
    1.18  val e_skolemize_rules = ["skolemize", "shift_quantors"]
    1.19  val spass_pirate_datatype_rule = "DT"
    1.20  val vampire_skolemisation_rule = "skolemisation"
    1.21 @@ -262,7 +266,7 @@
    1.22          val string_of_isar_proof =
    1.23            string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
    1.24  
    1.25 -        val trace = false
    1.26 +        val trace = Config.get ctxt trace
    1.27  
    1.28          val isar_proof =
    1.29            refute_graph
    1.30 @@ -273,13 +277,17 @@
    1.31            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.32            |> relabel_isar_proof_canonically
    1.33  
    1.34 -        val preplay_data as {overall_preplay_outcome, ...} =
    1.35 +        val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
    1.36            preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.37              preplay_timeout isar_proof
    1.38  
    1.39 +        fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
    1.40 +        fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
    1.41 +
    1.42          fun trace_isar_proof label proof =
    1.43            if trace then
    1.44 -            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof true proof ^ "\n")
    1.45 +            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
    1.46 +              "\n")
    1.47            else
    1.48              ()
    1.49  
    1.50 @@ -299,7 +307,7 @@
    1.51            ||> kill_useless_labels_in_isar_proof
    1.52            ||> relabel_isar_proof_finally
    1.53        in
    1.54 -        (case string_of_isar_proof false isar_proof of
    1.55 +        (case string_of_isar_proof (K (K "")) isar_proof of
    1.56            "" =>
    1.57            if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
    1.58            else ""