use configuration mechanism for low-level tracing

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -100,8 +100,7 @@
    ("isar_minimize", "true"), (* TODO: document *)
    ("slice", "true"),
    ("minimize", "smart"),
-   ("preplay_timeout", "3"),
-   ("preplay_trace", "false")] (* TODO: document *)
+   ("preplay_timeout", "3")]
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
@@ -120,8 +119,7 @@
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
    ("dont_try0_isar", "isar_try0"),
-   ("dont_minimize_isar", "isar_minimize"),
-   ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
+   ("dont_minimize_isar", "isar_minimize")]
 
 val params_not_for_minimize =
   ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice",
@@ -318,7 +316,6 @@
     val preplay_timeout =
       if mode = Auto_Try then SOME Time.zeroTime
       else lookup_time "preplay_timeout"
-    val preplay_trace = lookup_bool "preplay_trace"
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
@@ -331,7 +328,7 @@
      merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
      isar_minimize = isar_minimize, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
-     preplay_trace = preplay_trace, expect = expect}
+     expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -58,9 +58,8 @@
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
                  uncurried_aliases, isar_proofs, isar_compress,
-                 isar_compress_degree, merge_timeout_slack,
-                 isar_try0, isar_minimize,
-                 preplay_timeout, preplay_trace, ...} : params)
+                 isar_compress_degree, merge_timeout_slack, isar_try0,
+                 isar_minimize, preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
     val _ =
@@ -86,8 +85,7 @@
        merge_timeout_slack = merge_timeout_slack,
        isar_try0 = isar_try0, isar_minimize = isar_minimize,
        slice = false, minimize = SOME false, timeout = timeout,
-       preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
-       expect = ""}
+       preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -258,8 +256,8 @@
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
          fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
          isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0,
-         isar_minimize, slice,
-         minimize, timeout, preplay_timeout, preplay_trace, expect} : params) =
+         isar_minimize, slice, minimize, timeout, preplay_timeout, expect} :
+         params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -277,10 +275,9 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
      isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
-     merge_timeout_slack = merge_timeout_slack,
-     isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
-     preplay_trace = preplay_trace, expect = expect}
+     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
+     isar_minimize = isar_minimize, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -17,12 +17,11 @@
     PplFail of exn |
     PplSucc of preplay_time
 
+  val trace : bool Config.T
   val zero_preplay_time : preplay_time
   val some_preplay_time : preplay_time
   val add_preplay_time : preplay_time -> preplay_time -> preplay_time
   val string_of_preplay_time : preplay_time -> string
-  (*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
-    Time.time -> isar_step -> preplay_time*)
 
   type preplay_interface =
   { get_preplay_result : label -> preplay_result,
@@ -34,9 +33,8 @@
     overall_preplay_stats : isar_proof -> preplay_time * bool }
 
   val proof_preplay_interface :
-    bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
+    bool -> Proof.context -> string -> string -> bool -> Time.time
     -> isar_proof -> preplay_interface
-
 end
 
 structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
@@ -45,6 +43,9 @@
 open Sledgehammer_Util
 open Sledgehammer_Proof
 
+val trace =
+  Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
+
 (* The boolean flag encodes whether the time is exact (false) or an lower bound
    (true):
       (t, false) = "t ms"
@@ -77,7 +78,7 @@
                         |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
                         |> cons assms
                         |> cons time
-    val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)
+    val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
   in tracing (Pretty.string_of pretty_trace) end
 
 (* timing *)
@@ -132,8 +133,8 @@
 
 
 (* main function for preplaying isar_steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
-  | preplay_raw debug trace type_enc lam_trans ctxt timeout
+fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
+  | preplay_raw debug type_enc lam_trans ctxt timeout
       (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
   let
     val (prop, obtain) =
@@ -171,12 +172,12 @@
     val preplay_time = take_time timeout run_tac ()
   in
     (* tracing *)
-    (if trace then preplay_trace ctxt facts prop preplay_time else () ;
+    (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
+     else ();
      preplay_time)
   end
 
 
-
 (*** proof preplay interface ***)
 
 type preplay_interface =
@@ -216,13 +217,12 @@
    The preplay results are caluclated lazyly and cached to avoid repeated
    calculation.
 
-   PRE CONDITION: the proof must be labeled canocially, see
+   PRECONDITION: the proof must be labeled canocially, see
    Slegehammer_Proof.relabel_proof_canonically
 *)
 
-
 fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
-      preplay_timeout preplay_trace proof : preplay_interface =
+      preplay_timeout proof : preplay_interface =
   if not do_preplay then
     (* the dont_preplay option pretends that everything works just fine *)
     { get_preplay_result = K (PplSucc zero_preplay_time),
@@ -238,7 +238,7 @@
       val ctxt = enrich_context proof ctxt
 
       fun preplay quietly timeout step =
-        preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
+        preplay_raw debug type_enc lam_trans ctxt timeout step
         |> PplSucc
         handle exn =>
           if Exn.is_interrupt exn then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -44,7 +44,6 @@
      minimize : bool option,
      timeout : Time.time option,
      preplay_timeout : Time.time option,
-     preplay_trace : bool,
      expect : string}
 
   type relevance_fudge =
@@ -359,7 +358,6 @@
    minimize : bool option,
    timeout : Time.time option,
    preplay_timeout : Time.time option,
-   preplay_trace : bool,
    expect : string}
 
 type relevance_fudge =
@@ -682,8 +680,7 @@
                     uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_compress,
                     isar_compress_degree, merge_timeout_slack, isar_try0,
-                    isar_minimize, slice, timeout, preplay_timeout,
-                    preplay_trace, ...})
+                    isar_minimize, slice, timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -958,10 +955,10 @@
                   else
                     ()
                 val isar_params =
-                  (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)
+                  (debug, verbose, preplay_timeout, isar_compress,
+                   isar_compress_degree, merge_timeout_slack, isar_try0,
+                   isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
+                   goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command ctxt params minimize_command name

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -12,7 +12,7 @@
   type one_line_params = Sledgehammer_Print.one_line_params
 
   type isar_params =
-    bool * bool * Time.time option * bool * real * int * real * bool * bool
+    bool * bool * Time.time option * real * int * real * bool * bool
     * string Symtab.table * (string * stature) list vector
     * (string * term) list * int Symtab.table * string atp_proof * thm
 
@@ -408,14 +408,14 @@
   in chain_proof end
 
 type isar_params =
-  bool * bool * Time.time option * bool * real * int * real * bool * bool
+  bool * bool * Time.time option * real * int * real * bool * bool
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string atp_proof * thm
 
 fun isar_proof_text ctxt 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)
+    (debug, verbose, preplay_timeout, isar_compress, isar_compress_degree,
+     merge_timeout_slack, isar_try0, isar_minimize, pool, fact_names, lifted,
+     sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -580,13 +580,13 @@
           chain_direct_proof
           #> kill_useless_labels_in_proof
           #> relabel_proof
-        val (preplay_interface as { overall_preplay_stats, ... }, isar_proof) =
+        val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
           refute_graph
           |> redirect_graph axioms tainted bot
           |> isar_proof_of_direct_proof
           |> relabel_proof_canonically
           |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
-               preplay_timeout preplay_trace)
+               preplay_timeout)
         val ((preplay_time, preplay_fail), isar_proof) =
           isar_proof
           |> compress_proof