1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Gobject.Data
open Ideutils
exception Stop
exception Done
module MyMap = Map.Make (struct type t = string let compare = compare end)
class blaster_window (n:int) =
let window = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:320 ~height:200
~title:"Blaster Window" ~show:false ()
in
let box1 = GPack.vbox ~packing:window#add () in
let sw = GBin.scrolled_window ~packing:(box1#pack ~expand:true ~fill:true) () in
let cols = new GTree.column_list in
let argument = cols#add string in
let tactic = cols#add string in
let status = cols#add boolean in
let nb_goals = cols#add string in
let model = GTree.tree_store cols in
let new_arg s =
let row = model#append () in
model#set ~row ~column:argument s;
row
in
let new_tac arg s =
let row = model#append ~parent:arg () in
model#set ~row ~column:tactic s;
model#set ~row ~column:status false;
model#set ~row ~column:nb_goals "?";
row
in
let view = GTree.view ~model ~packing:sw#add () in
let _ = view#selection#set_mode `SINGLE in
let _ = view#set_rules_hint true in
let col = GTree.view_column ~title:"Argument" ()
~renderer:(GTree.cell_renderer_text [], ["text",argument]) in
let _ = view#append_column col in
let col = GTree.view_column ~title:"Tactics" ()
~renderer:(GTree.cell_renderer_text [], ["text",tactic]) in
let _ = view#append_column col in
let col = GTree.view_column ~title:"Status" ()
~renderer:(GTree.cell_renderer_toggle [], ["active",status]) in
let _ = view#append_column col in
let col = GTree.view_column ~title:"Delta Goal" ()
~renderer:(GTree.cell_renderer_text [], ["text",nb_goals]) in
let _ = view#append_column col in
let _ = GMisc.separator `HORIZONTAL ~packing:box1#pack () in
let box2 = GPack.vbox ~spacing: 10 ~border_width: 10 ~packing: box1#pack ()
in
let button_stop = GButton.button ~label: "Stop" ~packing: box2#add () in
let _ = button_stop#connect#clicked ~callback: window#misc#hide in
object(self)
val window = window
val roots = Hashtbl.create 17
val mutable tbl = MyMap.empty
val blaster_lock = Mutex.create ()
method lock = blaster_lock
val blaster_killed = Condition.create ()
method blaster_killed = blaster_killed
method window = window
method set
root
name
(compute:unit -> Coq.tried_tactic)
(on_click:unit -> unit)
=
let root_iter =
try Hashtbl.find roots root
with Not_found ->
let nr = new_arg root in
Hashtbl.add roots root nr;
nr
in
let nt = new_tac root_iter name in
let old_val = try MyMap.find root tbl with Not_found -> MyMap.empty in
tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl
method clear () =
model#clear ();
tbl <- MyMap.empty;
Hashtbl.clear roots;
method blaster () =
view#expand_all ();
try MyMap.iter
(fun root_name l ->
try
MyMap.iter
(fun name (nt,compute,on_click) ->
match compute () with
| Coq.Interrupted ->
prerr_endline "Interrupted";
raise Stop
| Coq.Failed ->
prerr_endline "Failed";
ignore (model#remove nt)
(* model#set ~row:nt ~column:status false;
model#set ~row:nt ~column:nb_goals "N/A"
*)
| Coq.Success n ->
prerr_endline "Success";
model#set ~row:nt ~column:status true;
model#set ~row:nt ~column:nb_goals (string_of_int n);
if n= -1 then raise Done
)
l
with Done -> ())
tbl;
Condition.signal blaster_killed;
prerr_endline "End of blaster";
with Stop ->
Condition.signal blaster_killed;
prerr_endline "End of blaster (stopped !)";
initializer
ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
ignore (view#selection#connect#after#changed ~callback:
begin fun () ->
prerr_endline "selection changed";
List.iter
(fun path ->let pt = GtkTree.TreePath.to_string path in
let it = model#get_iter path in
prerr_endline (string_of_bool (model#iter_is_valid it));
let name = model#get
~row:(if String.length pt >1 then begin
ignore (GtkTree.TreePath.up path);
model#get_iter path
end else it
)
~column:argument in
let tactic = model#get ~row:it ~column:tactic in
prerr_endline ("Got name: "^name);
let success = model#get ~row:it ~column:status in
if success then try
prerr_endline "Got success";
let _,_,f = MyMap.find tactic (MyMap.find name tbl) in
f ();
(* window#misc#hide () *)
with _ -> ()
)
view#selection#get_selected_rows
end);
(* needs lablgtk2 update ignore (view#connect#after#row_activated
(fun path vcol ->
prerr_endline "Activated";
);
*)
end
let blaster_window = ref None
let main n = blaster_window := Some (new blaster_window n)
let present_blaster_window () = match !blaster_window with
| None -> failwith "No blaster window."
| Some c -> c#window#misc#show (* present*) (); c
let blaster_window () = match !blaster_window with
| None -> failwith "No blaster window."
| Some c -> c
|
