# HG changeset patch
# User wenzelm
# Date 1307698763 -7200
# Node ID 911cb8242dfe531dca4fc09ba33e2a7880242b2e
# Parent  165188299a25a760adcd2fdecaf13e4a01098e39
more official options blast_trace, blast_stats;

diff -r 165188299a25 -r 911cb8242dfe src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Jun 09 23:30:18 2011 +0200
+++ b/src/Provers/blast.ML	Fri Jun 10 11:39:23 2011 +0200
@@ -63,8 +63,8 @@
   val setup: theory -> theory
   (*debugging tools*)
   type branch
+  val trace: bool Config.T
   val stats: bool Config.T
-  val trace: bool Config.T
   val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
   val fromTerm: theory -> Term.term -> term
   val fromSubgoal: theory -> Term.term -> term
@@ -82,9 +82,12 @@
 
 structure Classical = Data.Classical;
 
-val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false)));
-val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false)));
-(*for runtime and search statistics*)
+(* options *)
+
+val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
+val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
+val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
+
 
 datatype term =
     Const  of string * term list  (*typargs constant--as a terms!*)
@@ -1251,8 +1254,6 @@
           case Seq.pull(EVERY' (rev tacs) 1 st) of
               NONE => (writeln ("PROOF FAILED for depth " ^
                                 string_of_int lim);
-                       if trace then error "************************\n"
-                       else ();
                        backtrack trace choices)
             | cell => (if (trace orelse stats)
                        then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
@@ -1271,9 +1272,6 @@
       raw_blast (Timing.start ()) ctxt lim) i st;
 
 
-val (depth_limit, setup_depth_limit) =
-  Attrib.config_int @{binding blast_depth_limit} (K 20);
-
 fun blast_tac ctxt i st =
   let
     val start = Timing.start ();
@@ -1305,6 +1303,8 @@
 
 val setup =
   setup_depth_limit #>
+  setup_trace #>
+  setup_stats #>
   Method.setup @{binding blast}
     (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
       (fn NONE => SIMPLE_METHOD' o blast_tac