tuned signature;
authorwenzelm
Thu Apr 07 20:32:42 2011 +0200 (2011-04-07)
changeset 422777503beeffd8d
parent 42276 992892b48296
child 42278 088a2d69746f
tuned signature;
src/Pure/Isar/attrib.ML
src/Pure/Syntax/ast.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Apr 07 18:41:49 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Apr 07 20:32:42 2011 +0200
     1.3 @@ -398,8 +398,8 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val _ = Context.>> (Context.map_theory
     1.7 - (register_config Ast.ast_trace_raw #>
     1.8 -  register_config Ast.ast_stat_raw #>
     1.9 + (register_config Ast.trace_raw #>
    1.10 +  register_config Ast.stat_raw #>
    1.11    register_config Syntax.positions_raw #>
    1.12    register_config Syntax.show_brackets_raw #>
    1.13    register_config Syntax.show_sorts_raw #>
     2.1 --- a/src/Pure/Syntax/ast.ML	Thu Apr 07 18:41:49 2011 +0200
     2.2 +++ b/src/Pure/Syntax/ast.ML	Thu Apr 07 20:32:42 2011 +0200
     2.3 @@ -21,10 +21,10 @@
     2.4    val fold_ast_p: string -> ast list * ast -> ast
     2.5    val unfold_ast: string -> ast -> ast list
     2.6    val unfold_ast_p: string -> ast -> ast list * ast
     2.7 -  val ast_trace_raw: Config.raw
     2.8 -  val ast_trace: bool Config.T
     2.9 -  val ast_stat_raw: Config.raw
    2.10 -  val ast_stat: bool Config.T
    2.11 +  val trace_raw: Config.raw
    2.12 +  val trace: bool Config.T
    2.13 +  val stat_raw: Config.raw
    2.14 +  val stat: bool Config.T
    2.15    val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
    2.16  end;
    2.17  
    2.18 @@ -164,11 +164,11 @@
    2.19  
    2.20  (* normalize *)
    2.21  
    2.22 -val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
    2.23 -val ast_trace = Config.bool ast_trace_raw;
    2.24 +val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
    2.25 +val trace = Config.bool trace_raw;
    2.26  
    2.27 -val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
    2.28 -val ast_stat = Config.bool ast_stat_raw;
    2.29 +val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
    2.30 +val stat = Config.bool stat_raw;
    2.31  
    2.32  fun message head body =
    2.33    Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
    2.34 @@ -176,8 +176,8 @@
    2.35  (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
    2.36  fun normalize ctxt get_rules pre_ast =
    2.37    let
    2.38 -    val trace = Config.get ctxt ast_trace;
    2.39 -    val stat = Config.get ctxt ast_stat;
    2.40 +    val trace = Config.get ctxt trace;
    2.41 +    val stat = Config.get ctxt stat;
    2.42  
    2.43      val passes = Unsynchronized.ref 0;
    2.44      val failed_matches = Unsynchronized.ref 0;