--- a/NEWS Tue Dec 21 21:31:36 2010 +0100
+++ b/NEWS Tue Dec 21 21:54:51 2010 +0100
@@ -54,13 +54,15 @@
show_consts show_consts
show_abbrevs show_abbrevs
- Syntax.trace_ast syntax_ast_trace
- Syntax.stat_ast syntax_ast_stat
+ Syntax.ast_trace syntax_ast_trace
+ Syntax.ast_stat syntax_ast_stat
Syntax.ambiguity_level syntax_ambiguity_level
Goal_Display.goals_limit goals_limit
Goal_Display.show_main_goal show_main_goal
+ Method.rule_trace rule_trace
+
Thy_Output.display thy_output_display
Thy_Output.quotes thy_output_quotes
Thy_Output.indent thy_output_indent
--- a/src/Pure/Isar/method.ML Tue Dec 21 21:31:36 2010 +0100
+++ b/src/Pure/Isar/method.ML Tue Dec 21 21:54:51 2010 +0100
@@ -8,7 +8,7 @@
sig
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val trace_rules: bool Unsynchronized.ref
+ val rule_trace: bool Config.T
end;
signature METHOD =
@@ -218,10 +218,10 @@
(* rule etc. -- single-step refinements *)
-val trace_rules = Unsynchronized.ref false;
+val (rule_trace, rule_trace_setup) = Attrib.config_bool "rule_trace" (fn _ => false);
fun trace ctxt rules =
- if ! trace_rules andalso not (null rules) then
+ if Config.get ctxt rule_trace andalso not (null rules) then
Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
|> Pretty.string_of |> tracing
else ();
@@ -438,7 +438,8 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+ (rule_trace_setup #>
+ setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
setup (Binding.name "-") (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
--- a/src/Pure/ProofGeneral/preferences.ML Tue Dec 21 21:31:36 2010 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Tue Dec 21 21:54:51 2010 +0100
@@ -153,9 +153,6 @@
nat_pref Raw_Simplifier.simp_trace_depth_limit_default
"trace-simplifier-depth"
"Trace simplifier depth limit.",
- bool_pref trace_rules
- "trace-rules"
- "Trace application of the standard rules",
bool_pref Pattern.trace_unify_fail
"trace-unification"
"Output error diagnostics during unification",