src/Pure/Syntax/ast.ML

--- a/src/Pure/Syntax/ast.ML	Tue Dec 21 21:05:50 2010 +0100
+++ b/src/Pure/Syntax/ast.ML	Tue Dec 21 21:21:21 2010 +0100
@@ -24,8 +24,10 @@
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
-  val trace_ast: bool Unsynchronized.ref
-  val stat_ast: bool Unsynchronized.ref
+  val ast_trace_raw: Config.raw
+  val ast_trace: bool Config.T
+  val ast_stat_raw: Config.raw
+  val ast_stat: bool Config.T
 end;
 
 signature AST =
@@ -33,8 +35,7 @@
   include AST1
   val head_of_rule: ast * ast -> string
   val rule_error: ast * ast -> string option
-  val normalize: bool -> bool -> (string -> (ast * ast) list) -> ast -> ast
-  val normalize_ast: (string -> (ast * ast) list) -> ast -> ast
+  val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
 
 structure Ast : AST =
@@ -168,10 +169,18 @@
 
 (* normalize *)
 
-(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
+val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
+val ast_trace = Config.bool ast_trace_raw;
+
+val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
+val ast_stat = Config.bool ast_stat_raw;
 
-fun normalize trace stat get_rules pre_ast =
+(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
+fun normalize ctxt get_rules pre_ast =
   let
+    val trace = Config.get ctxt ast_trace;
+    val stat = Config.get ctxt ast_stat;
+
     val passes = Unsynchronized.ref 0;
     val failed_matches = Unsynchronized.ref 0;
     val changes = Unsynchronized.ref 0;
@@ -241,13 +250,4 @@
       else ();
   in post_ast end;
 
-
-(* normalize_ast *)
-
-val trace_ast = Unsynchronized.ref false;
-val stat_ast = Unsynchronized.ref false;
-
-fun normalize_ast get_rules ast =
-  normalize (! trace_ast) (! stat_ast) get_rules ast;
-
 end;