configuration option "syntax_ast_trace" and "syntax_ast_stat";

--- a/NEWS	Tue Dec 21 21:05:50 2010 +0100
+++ b/NEWS	Tue Dec 21 21:21:21 2010 +0100
@@ -54,6 +54,8 @@
   show_consts                   show_consts
   show_abbrevs                  show_abbrevs
 
+  Syntax.trace_ast              syntax_ast_trace
+  Syntax.stat_ast               syntax_ast_stat
   Syntax.ambiguity_level        syntax_ambiguity_level
 
   Goal_Display.goals_limit      goals_limit

--- a/src/Pure/Isar/attrib.ML	Tue Dec 21 21:05:50 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Dec 21 21:21:21 2010 +0100
@@ -398,7 +398,9 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_brackets_raw #>
+ (register_config Syntax.ast_trace_raw #>
+  register_config Syntax.ast_stat_raw #>
+  register_config Syntax.show_brackets_raw #>
   register_config Syntax.show_sorts_raw #>
   register_config Syntax.show_types_raw #>
   register_config Syntax.show_structs_raw #>

--- 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;

--- a/src/Pure/Syntax/syntax.ML	Tue Dec 21 21:05:50 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Dec 21 21:21:21 2010 +0100
@@ -736,7 +736,7 @@
     val asts = read_asts ctxt syn false root inp;
   in
     Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
-      (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
+      (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
   end;
 
 
@@ -871,7 +871,7 @@
   in
     Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (print_mode_value ()))
-      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
+      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
   end;
 
 in