tuned name (cf. blast_stats);
authorwenzelm
Fri Jun 10 11:47:52 2011 +0200 (2011-06-10)
changeset 43347f18cf88453d6
parent 43346 911cb8242dfe
child 43348 3e153e719039
tuned name (cf. blast_stats);
src/Pure/Isar/attrib.ML
src/Pure/Syntax/ast.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 10 11:39:23 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 10 11:47:52 2011 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4  
     1.5  val _ = Context.>> (Context.map_theory
     1.6   (register_config Ast.trace_raw #>
     1.7 -  register_config Ast.stat_raw #>
     1.8 +  register_config Ast.stats_raw #>
     1.9    register_config Syntax.positions_raw #>
    1.10    register_config Printer.show_brackets_raw #>
    1.11    register_config Printer.show_sorts_raw #>
     2.1 --- a/src/Pure/Syntax/ast.ML	Fri Jun 10 11:39:23 2011 +0200
     2.2 +++ b/src/Pure/Syntax/ast.ML	Fri Jun 10 11:47:52 2011 +0200
     2.3 @@ -23,8 +23,8 @@
     2.4    val unfold_ast_p: string -> ast -> ast list * ast
     2.5    val trace_raw: Config.raw
     2.6    val trace: bool Config.T
     2.7 -  val stat_raw: Config.raw
     2.8 -  val stat: bool Config.T
     2.9 +  val stats_raw: Config.raw
    2.10 +  val stats: bool Config.T
    2.11    val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
    2.12  end;
    2.13  
    2.14 @@ -167,8 +167,8 @@
    2.15  val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
    2.16  val trace = Config.bool trace_raw;
    2.17  
    2.18 -val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
    2.19 -val stat = Config.bool stat_raw;
    2.20 +val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
    2.21 +val stats = Config.bool stats_raw;
    2.22  
    2.23  fun message head body =
    2.24    Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
    2.25 @@ -177,7 +177,7 @@
    2.26  fun normalize ctxt get_rules pre_ast =
    2.27    let
    2.28      val trace = Config.get ctxt trace;
    2.29 -    val stat = Config.get ctxt stat;
    2.30 +    val stats = Config.get ctxt stats;
    2.31  
    2.32      val passes = Unsynchronized.ref 0;
    2.33      val failed_matches = Unsynchronized.ref 0;
    2.34 @@ -239,7 +239,7 @@
    2.35      val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
    2.36      val post_ast = normal pre_ast;
    2.37      val _ =
    2.38 -      if trace orelse stat then
    2.39 +      if trace orelse stats then
    2.40          tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
    2.41            string_of_int (! passes) ^ " passes, " ^
    2.42            string_of_int (! changes) ^ " changes, " ^