| author | blanchet |
| Mon, 20 Jan 2014 20:00:33 +0100 | |
| changeset 55082 | e60036c1c248 |
| parent 54731 | 384ac33802b0 |
| child 55316 | 885500f4aa6a |
| permissions | -rw-r--r-- |
| 54730 | 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 |
|
|
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54730
diff
changeset
|
21 |
(Simplifier.set_trace_ops |
| 54730 | 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)
|
|
|
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54730
diff
changeset
|
30 |
else (); cont ctxt)}) |
| 54730 | 31 |
|
32 |
||
33 |
(* PIDE protocol *) |
|
34 |
||
35 |
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
|
36 |
||
37 |
end |
|
38 |