equal
deleted
inserted
replaced
48 struct |
48 struct |
49 (**) |
49 (**) |
50 |
50 |
51 exception NO_REWRITE; |
51 exception NO_REWRITE; |
52 |
52 |
53 (* depth of recursion in traces of the rewriter, if trace_on:=true *) |
53 (* depth of recursion in traces of the rewriter, if trace_on = true *) |
54 val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999); |
54 val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999); |
55 |
55 |
56 fun trace ctxt i str = |
56 fun trace ctxt i str = |
57 if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth |
57 if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth |
58 then tracing (idt "#" i ^ str) else () |
58 then tracing (idt "#" i ^ str) else () |