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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: blaster_window.ml 8912 2006-06-07 11:20:58Z notin $ *)
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
|