# HG changeset patch # User wenzelm # Date 1292962881 -3600 # Node ID 390c539042205624058979b14de296fabba078dd # Parent 08240feb69c77fdffaad62fe35746c75c9f1b5f6 configuration option "syntax_ast_trace" and "syntax_ast_stat"; diff -r 08240feb69c7 -r 390c53904220 NEWS --- 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 diff -r 08240feb69c7 -r 390c53904220 src/Pure/Isar/attrib.ML --- 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 #> diff -r 08240feb69c7 -r 390c53904220 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; diff -r 08240feb69c7 -r 390c53904220 src/Pure/Syntax/syntax.ML --- 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