1.1 --- a/NEWS	Tue Dec 21 21:05:50 2010 +0100
     1.2 +++ b/NEWS	Tue Dec 21 21:21:21 2010 +0100
     1.3 @@ -54,6 +54,8 @@
     1.4    show_consts                   show_consts
     1.5    show_abbrevs                  show_abbrevs
     1.6  
     1.7 +  Syntax.trace_ast              syntax_ast_trace
     1.8 +  Syntax.stat_ast               syntax_ast_stat
     1.9    Syntax.ambiguity_level        syntax_ambiguity_level
    1.10  
    1.11    Goal_Display.goals_limit      goals_limit

     2.1 --- a/src/Pure/Isar/attrib.ML	Tue Dec 21 21:05:50 2010 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Tue Dec 21 21:21:21 2010 +0100
     2.3 @@ -398,7 +398,9 @@
     2.4  (* theory setup *)
     2.5  
     2.6  val _ = Context.>> (Context.map_theory
     2.7 - (register_config Syntax.show_brackets_raw #>
     2.8 + (register_config Syntax.ast_trace_raw #>
     2.9 +  register_config Syntax.ast_stat_raw #>
    2.10 +  register_config Syntax.show_brackets_raw #>
    2.11    register_config Syntax.show_sorts_raw #>
    2.12    register_config Syntax.show_types_raw #>
    2.13    register_config Syntax.show_structs_raw #>

     3.1 --- a/src/Pure/Syntax/ast.ML	Tue Dec 21 21:05:50 2010 +0100
     3.2 +++ b/src/Pure/Syntax/ast.ML	Tue Dec 21 21:21:21 2010 +0100
     3.3 @@ -24,8 +24,10 @@
     3.4    val fold_ast_p: string -> ast list * ast -> ast
     3.5    val unfold_ast: string -> ast -> ast list
     3.6    val unfold_ast_p: string -> ast -> ast list * ast
     3.7 -  val trace_ast: bool Unsynchronized.ref
     3.8 -  val stat_ast: bool Unsynchronized.ref
     3.9 +  val ast_trace_raw: Config.raw
    3.10 +  val ast_trace: bool Config.T
    3.11 +  val ast_stat_raw: Config.raw
    3.12 +  val ast_stat: bool Config.T
    3.13  end;
    3.14  
    3.15  signature AST =
    3.16 @@ -33,8 +35,7 @@
    3.17    include AST1
    3.18    val head_of_rule: ast * ast -> string
    3.19    val rule_error: ast * ast -> string option
    3.20 -  val normalize: bool -> bool -> (string -> (ast * ast) list) -> ast -> ast
    3.21 -  val normalize_ast: (string -> (ast * ast) list) -> ast -> ast
    3.22 +  val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
    3.23  end;
    3.24  
    3.25  structure Ast : AST =
    3.26 @@ -168,10 +169,18 @@
    3.27  
    3.28  (* normalize *)
    3.29  
    3.30 +val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
    3.31 +val ast_trace = Config.bool ast_trace_raw;
    3.32 +
    3.33 +val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
    3.34 +val ast_stat = Config.bool ast_stat_raw;
    3.35 +
    3.36  (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
    3.37 +fun normalize ctxt get_rules pre_ast =
    3.38 +  let
    3.39 +    val trace = Config.get ctxt ast_trace;
    3.40 +    val stat = Config.get ctxt ast_stat;
    3.41  
    3.42 -fun normalize trace stat get_rules pre_ast =
    3.43 -  let
    3.44      val passes = Unsynchronized.ref 0;
    3.45      val failed_matches = Unsynchronized.ref 0;
    3.46      val changes = Unsynchronized.ref 0;
    3.47 @@ -241,13 +250,4 @@
    3.48        else ();
    3.49    in post_ast end;
    3.50  
    3.51 -
    3.52 -(* normalize_ast *)
    3.53 -
    3.54 -val trace_ast = Unsynchronized.ref false;
    3.55 -val stat_ast = Unsynchronized.ref false;
    3.56 -
    3.57 -fun normalize_ast get_rules ast =
    3.58 -  normalize (! trace_ast) (! stat_ast) get_rules ast;
    3.59 -
    3.60  end;

     4.1 --- a/src/Pure/Syntax/syntax.ML	Tue Dec 21 21:05:50 2010 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Dec 21 21:21:21 2010 +0100
     4.3 @@ -736,7 +736,7 @@
     4.4      val asts = read_asts ctxt syn false root inp;
     4.5    in
     4.6      Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
     4.7 -      (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
     4.8 +      (map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) asts)
     4.9    end;
    4.10  
    4.11  
    4.12 @@ -871,7 +871,7 @@
    4.13    in
    4.14      Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
    4.15        (lookup_tokentr tokentrtab (print_mode_value ()))
    4.16 -      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
    4.17 +      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
    4.18    end;
    4.19  
    4.20  in