author | Lars Hupel <lars.hupel@mytum.de> |
Wed, 05 Feb 2014 15:44:32 +0100 | |
changeset 55335 | 8192d3acadbe |
parent 55316 | 885500f4aa6a |
child 55390 | 36550a4eac5e |
permissions | -rw-r--r-- |
54730 | 1 |
(* Title: Pure/Tools/simplifier_trace.ML |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
2 |
Author: Lars Hupel |
54730 | 3 |
|
4 |
Interactive Simplifier trace. |
|
5 |
*) |
|
6 |
||
7 |
signature SIMPLIFIER_TRACE = |
|
8 |
sig |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
9 |
val add_term_breakpoint: term -> Context.generic -> Context.generic |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
10 |
val add_thm_breakpoint: thm -> Context.generic -> Context.generic |
54730 | 11 |
end |
12 |
||
13 |
structure Simplifier_Trace: SIMPLIFIER_TRACE = |
|
14 |
struct |
|
15 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
16 |
(** background data **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
17 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
18 |
datatype mode = Disabled | Normal | Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
19 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
20 |
fun merge_modes Disabled m = m |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
21 |
| merge_modes Normal Full = Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
22 |
| merge_modes Normal _ = Normal |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
23 |
| merge_modes Full _ = Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
24 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
25 |
val empty_breakpoints = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
26 |
(Item_Net.init (op =) single (* FIXME equality on terms? *), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
27 |
Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
28 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
29 |
fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
30 |
(Item_Net.merge (term_bs1, term_bs2), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
31 |
Item_Net.merge (thm_bs1, thm_bs2)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
32 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
33 |
structure Data = Generic_Data |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
34 |
( |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
35 |
type T = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
36 |
{max_depth: int, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
37 |
depth: int, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
38 |
mode: mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
39 |
interactive: bool, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
40 |
parent: int, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
41 |
breakpoints: term Item_Net.T * rrule Item_Net.T} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
42 |
val empty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
43 |
{max_depth = 10, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
44 |
depth = 0, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
45 |
mode = Disabled, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
46 |
interactive = false, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
47 |
parent = 0, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
48 |
breakpoints = empty_breakpoints} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
49 |
val extend = I |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
50 |
fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, |
55335 | 51 |
breakpoints = breakpoints1, ...}: T, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
52 |
{max_depth = max_depth2, mode = mode2, interactive = interactive2, |
55335 | 53 |
breakpoints = breakpoints2, ...}: T) = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
54 |
{max_depth = Int.max (max_depth1, max_depth2), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
55 |
depth = 0, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
56 |
mode = merge_modes mode1 mode2, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
57 |
interactive = interactive1 orelse interactive2, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
58 |
parent = 0, |
55335 | 59 |
breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
60 |
) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
61 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
62 |
fun map_breakpoints f_term f_thm = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
63 |
Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
64 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
65 |
depth = depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
66 |
mode = mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
67 |
interactive = interactive, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
68 |
parent = parent, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
69 |
breakpoints = (f_term term_bs, f_thm thm_bs)}) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
70 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
71 |
fun add_term_breakpoint term = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
72 |
map_breakpoints (Item_Net.update term) I |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
73 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
74 |
fun add_thm_breakpoint thm context = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
75 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
76 |
val rrules = mk_rrules (Context.proof_of context) [thm] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
77 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
78 |
map_breakpoints I (fold Item_Net.update rrules) context |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
79 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
80 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
81 |
fun is_breakpoint (term, rrule) context = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
82 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
83 |
val {breakpoints, ...} = Data.get context |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
84 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
85 |
fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
86 |
val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
87 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
88 |
val {thm = thm, ...} = rrule |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
89 |
val thm_matches = exists (eq_rrule o pair rrule) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
90 |
(Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
91 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
92 |
(term_matches, thm_matches) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
93 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
94 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
95 |
(** config and attributes **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
96 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
97 |
fun config raw_mode interactive max_depth = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
98 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
99 |
val mode = case raw_mode of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
100 |
"normal" => Normal |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
101 |
| "full" => Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
102 |
| _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
103 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
104 |
val update = Data.map (fn {depth, parent, breakpoints, ...} => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
105 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
106 |
depth = depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
107 |
mode = mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
108 |
interactive = interactive, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
109 |
parent = parent, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
110 |
breakpoints = breakpoints}) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
111 |
in Thm.declaration_attribute (K update) end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
112 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
113 |
fun term_breakpoint terms = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
114 |
Thm.declaration_attribute (K (fold add_term_breakpoint terms)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
115 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
116 |
val thm_breakpoint = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
117 |
Thm.declaration_attribute add_thm_breakpoint |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
118 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
119 |
(** tracing state **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
120 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
121 |
val futures = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
122 |
Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
123 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
124 |
(** markup **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
125 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
126 |
fun output_result (id, data) = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
127 |
Output.result (Markup.serial_properties id) data |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
128 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
129 |
val serialN = "serial" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
130 |
val parentN = "parent" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
131 |
val textN = "text" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
132 |
val successN = "success" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
133 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
134 |
val logN = "simp_trace_log" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
135 |
val stepN = "simp_trace_step" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
136 |
val recurseN = "simp_trace_recurse" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
137 |
val hintN = "simp_trace_hint" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
138 |
val ignoreN = "simp_trace_ignore" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
139 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
140 |
val cancelN = "simp_trace_cancel" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
141 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
142 |
type payload = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
143 |
{props: Properties.T, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
144 |
pretty: Pretty.T} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
145 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
146 |
fun empty_payload () : payload = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
147 |
{props = [], pretty = Pretty.str ""} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
148 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
149 |
fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
150 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
151 |
val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
152 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
153 |
val eligible = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
154 |
case mode of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
155 |
Disabled => false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
156 |
| Normal => triggered |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
157 |
| Full => true |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
158 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
159 |
val markup' = if markup = stepN andalso not interactive then logN else markup |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
160 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
161 |
if not eligible orelse depth > max_depth then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
162 |
NONE |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
163 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
164 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
165 |
val {props = more_props, pretty} = payload () |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
166 |
val props = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
167 |
[(textN, text), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
168 |
(parentN, Markup.print_int parent)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
169 |
val data = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
170 |
Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty]) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
171 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
172 |
SOME (serial (), data) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
173 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
174 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
175 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
176 |
(** tracing output **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
177 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
178 |
fun send_request (result_id, content) = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
179 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
180 |
fun break () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
181 |
(Output.protocol_message |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
182 |
[(Markup.functionN, cancelN), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
183 |
(serialN, Markup.print_int result_id)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
184 |
""; |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
185 |
Synchronized.change futures (Inttab.delete_safe result_id)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
186 |
val promise = Future.promise break : string future |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
187 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
188 |
Synchronized.change futures (Inttab.update_new (result_id, promise)); |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
189 |
output_result (result_id, content); |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
190 |
promise |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
191 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
192 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
193 |
|
55335 | 194 |
type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule} |
195 |
||
196 |
fun step ({term, thm, unconditional, ctxt, rrule}: data) = |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
197 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
198 |
val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
199 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
200 |
val {name, ...} = rrule |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
201 |
val term_triggered = not (null matching_terms) |
54730 | 202 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
203 |
val text = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
204 |
if unconditional then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
205 |
"Apply rewrite rule?" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
206 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
207 |
"Apply conditional rewrite rule?" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
208 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
209 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
210 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
211 |
(* FIXME pretty printing via Proof_Context.pretty_fact *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
212 |
val pretty_thm = Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
213 |
[Pretty.str ("Instance of " ^ name ^ ":"), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
214 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
215 |
Syntax.pretty_term ctxt (Thm.prop_of thm)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
216 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
217 |
val pretty_term = Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
218 |
[Pretty.str "Trying to rewrite:", |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
219 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
220 |
Syntax.pretty_term ctxt term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
221 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
222 |
val pretty_matchings = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
223 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
224 |
val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
225 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
226 |
if not (null matching_terms) then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
227 |
[Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
228 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
229 |
[] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
230 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
231 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
232 |
val pretty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
233 |
Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
234 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
235 |
{props = [], pretty = pretty} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
236 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
237 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
238 |
val {max_depth, depth, mode, interactive, breakpoints, ...} = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
239 |
Data.get (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
240 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
241 |
fun mk_promise result = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
242 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
243 |
val result_id = #1 result |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
244 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
245 |
fun put mode' interactive' = Data.put |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
246 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
247 |
depth = depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
248 |
mode = mode', |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
249 |
interactive = interactive', |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
250 |
parent = result_id, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
251 |
breakpoints = breakpoints} (Context.Proof ctxt) |> |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
252 |
Context.the_proof |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
253 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
254 |
fun to_response "skip" = NONE |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
255 |
| to_response "continue" = SOME (put mode true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
256 |
| to_response "continue_trace" = SOME (put Full true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
257 |
| to_response "continue_passive" = SOME (put mode false) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
258 |
| to_response "continue_disable" = SOME (put Disabled false) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
259 |
| to_response _ = raise Fail "Simplifier_Trace.step: invalid message" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
260 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
261 |
if not interactive then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
262 |
(output_result result; Future.value (SOME (put mode false))) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
263 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
264 |
Future.map to_response (send_request result) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
265 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
266 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
267 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
268 |
case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
269 |
NONE => Future.value (SOME ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
270 |
| SOME res => mk_promise res |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
271 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
272 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
273 |
fun recurse text term ctxt = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
274 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
275 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
276 |
{props = [], |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
277 |
pretty = Syntax.pretty_term ctxt term} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
278 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
279 |
val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
280 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
281 |
fun put result_id = Data.put |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
282 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
283 |
depth = depth + 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
284 |
mode = if depth >= max_depth then Disabled else mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
285 |
interactive = interactive, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
286 |
parent = result_id, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
287 |
breakpoints = breakpoints} (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
288 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
289 |
val context' = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
290 |
case mk_generic_result recurseN text true payload ctxt of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
291 |
NONE => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
292 |
put 0 |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
293 |
| SOME res => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
294 |
(output_result res; put (#1 res)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
295 |
in Context.the_proof context' end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
296 |
|
55335 | 297 |
fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
298 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
299 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
300 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
301 |
val {name, ...} = rrule |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
302 |
val pretty_thm = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
303 |
(* FIXME pretty printing via Proof_Context.pretty_fact *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
304 |
Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
305 |
[Pretty.str ("In an instance of " ^ name ^ ":"), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
306 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
307 |
Syntax.pretty_term ctxt (Thm.prop_of thm)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
308 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
309 |
val pretty_term = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
310 |
Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
311 |
[Pretty.str "Was trying to rewrite:", |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
312 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
313 |
Syntax.pretty_term ctxt term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
314 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
315 |
val pretty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
316 |
Pretty.chunks [pretty_thm, pretty_term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
317 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
318 |
{props = [(successN, "false")], pretty = pretty} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
319 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
320 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
321 |
val {interactive, ...} = Data.get (Context.Proof ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
322 |
val {parent, ...} = Data.get (Context.Proof ctxt') |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
323 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
324 |
fun mk_promise result = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
325 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
326 |
val result_id = #1 result |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
327 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
328 |
fun to_response "exit" = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
329 |
false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
330 |
| to_response "redo" = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
331 |
(Option.app output_result |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
332 |
(mk_generic_result ignoreN "Ignore" true empty_payload ctxt'); |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
333 |
true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
334 |
| to_response _ = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
335 |
raise Fail "Simplifier_Trace.indicate_failure: invalid message" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
336 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
337 |
if not interactive then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
338 |
(output_result result; Future.value false) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
339 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
340 |
Future.map to_response (send_request result) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
341 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
342 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
343 |
case mk_generic_result hintN "Step failed" true payload ctxt' of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
344 |
NONE => Future.value false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
345 |
| SOME res => mk_promise res |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
346 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
347 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
348 |
fun indicate_success thm ctxt = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
349 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
350 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
351 |
{props = [(successN, "true")], |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
352 |
pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
353 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
354 |
Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
355 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
356 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
357 |
(** setup **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
358 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
359 |
fun simp_if_continue args ctxt cont = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
360 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
361 |
val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
362 |
val data = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
363 |
{term = term, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
364 |
unconditional = unconditional, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
365 |
ctxt = ctxt, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
366 |
thm = thm, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
367 |
rrule = rrule} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
368 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
369 |
case Future.join (step data) of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
370 |
NONE => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
371 |
NONE |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
372 |
| SOME ctxt' => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
373 |
let val res = cont ctxt' in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
374 |
case res of |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
375 |
NONE => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
376 |
if Future.join (indicate_failure data ctxt') then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
377 |
simp_if_continue args ctxt cont |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
378 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
379 |
NONE |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
380 |
| SOME (thm, _) => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
381 |
(indicate_success thm ctxt'; |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
382 |
res) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
383 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
384 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
385 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
386 |
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
54730 | 387 |
|
388 |
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
|
389 |
(Simplifier.set_trace_ops |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
390 |
{trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
391 |
trace_apply = simp_if_continue}) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
392 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
393 |
val _ = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
394 |
Isabelle_Process.protocol_command "Document.simp_trace_reply" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
395 |
(fn [s, r] => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
396 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
397 |
val serial = Markup.parse_int s |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
398 |
fun lookup_delete tab = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
399 |
(Inttab.lookup tab serial, Inttab.delete_safe serial tab) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
400 |
fun apply_result (SOME promise) = Future.fulfill promise r |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
401 |
| apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
402 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
403 |
(Synchronized.change_result futures lookup_delete |> apply_result) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
404 |
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
405 |
end) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
406 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
407 |
(** attributes **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
408 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
409 |
val pat_parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
410 |
Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic |
54730 | 411 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
412 |
val mode_parser: string parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
413 |
Scan.optional |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
414 |
(Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
415 |
"normal" |
54730 | 416 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
417 |
val interactive_parser: bool parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
418 |
Scan.optional (Args.$$$ "interactive" >> K true) false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
419 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
420 |
val depth_parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
421 |
Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10 |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
422 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
423 |
val config_parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
424 |
(interactive_parser -- mode_parser -- depth_parser) >> |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
425 |
(fn ((interactive, mode), depth) => config mode interactive depth) |
54730 | 426 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
427 |
val _ = Theory.setup |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
428 |
(Attrib.setup @{binding break_term} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
429 |
((Scan.repeat1 pat_parser) >> term_breakpoint) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
430 |
"declaration of a term breakpoint" #> |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
431 |
Attrib.setup @{binding break_thm} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
432 |
(Scan.succeed thm_breakpoint) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
433 |
"declaration of a theorem breakpoint" #> |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
434 |
Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
435 |
"simplifier trace configuration") |
54730 | 436 |
|
437 |
end |