diff options
Diffstat (limited to 'ide/blaster_window.ml')
| -rw-r--r-- | ide/blaster_window.ml | 178 |
1 files changed, 0 insertions, 178 deletions
diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml deleted file mode 100644 index f3cb1e60..00000000 --- a/ide/blaster_window.ml +++ /dev/null @@ -1,178 +0,0 @@ -(************************************************************************) -(* 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 - - |