equal
deleted
inserted
replaced
|
1 (* Title: Pure/Tools/simplifier_trace.ML |
|
2 Author: Lars Hupel, TU Muenchen |
|
3 |
|
4 Interactive Simplifier trace. |
|
5 *) |
|
6 |
|
7 signature SIMPLIFIER_TRACE = |
|
8 sig |
|
9 val simp_trace_test: bool Config.T |
|
10 end |
|
11 |
|
12 structure Simplifier_Trace: SIMPLIFIER_TRACE = |
|
13 struct |
|
14 |
|
15 (* Simplifier trace operations *) |
|
16 |
|
17 val simp_trace_test = |
|
18 Attrib.setup_config_bool @{binding simp_trace_test} (K false) |
|
19 |
|
20 val _ = Theory.setup |
|
21 (Simplifier.map_theory_simpset (Simplifier.set_trace_ops |
|
22 {trace_invoke = fn {depth, term} => fn ctxt => |
|
23 (if Config.get ctxt simp_trace_test then |
|
24 tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^ |
|
25 Syntax.string_of_term ctxt term) |
|
26 else (); ctxt), |
|
27 trace_apply = fn args => fn ctxt => fn cont => |
|
28 (if Config.get ctxt simp_trace_test then |
|
29 tracing ("Simplifier " ^ @{make_string} args) |
|
30 else (); cont ctxt)})) |
|
31 |
|
32 |
|
33 (* PIDE protocol *) |
|
34 |
|
35 val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
|
36 |
|
37 end |
|
38 |