coqide: blaster 2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4067 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 77 insertions, 2 deletions

diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
new file mode 100644
index 000000000..32a1c6485
--- /dev/null
+++ b/ide/blaster_window.ml
@@ -0,0 +1,74 @@
+(***********************************************************************)
+(*  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$ *)
+
+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 table = GPack.table ~rows:(n/4+1) ~columns:4 ~homogeneous:false 
+		~row_spacings:3 ~col_spacings:3 ~border_width:10
+		~packing:box1#add () 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
+
+  let buttons = Array.create n ((GButton.button ~label:"Nothing" ()),(fun () -> Coq.Interrupted)) 
+  in
+  
+object(self)
+  val window = window
+  val buttons = buttons
+  method window = window
+  method buttons = buttons
+  method set i name (compute:unit -> Coq.tried_tactic) (on_click:unit -> unit) = 
+    let button = GButton.button ~label: (name) () in
+    buttons.(i) <- (button,compute);
+    let x = i/4 in
+    let y = i mod 4 in
+    table#attach button#coerce 
+      ~left:x ~top:y
+      ~xpadding:0 ~ypadding:0 ~expand:`BOTH;
+    ignore (button#connect#clicked ~callback:on_click)
+
+  method blaster () = 
+    for i = 0 to n-1 do 
+      let b,f = buttons.(i) in
+      GtkButton.Button.set_label (Obj.magic b#as_widget) 
+	(GtkButton.Button.get_label (Obj.magic b#as_widget)^": ");
+      match f () with 
+      | Coq.Interrupted -> 
+	  prerr_endline "Interrupted"
+      | Coq.Failed -> 
+	  prerr_endline "Failed"
+      | Coq.Success n -> 
+	  GtkButton.Button.set_label (Obj.magic b#as_widget) 
+	  (GtkButton.Button.get_label (Obj.magic b#as_widget)^ (string_of_int n));
+    done
+  initializer 
+    ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
+end
+
+let blaster_window = ref None
+
+let main n = blaster_window := Some (new blaster_window n)
+
+let blaster_window () = match !blaster_window with 
+  | None -> failwith "No blaster window."
+  | Some c -> c#window#present (); c
+
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6d96fc300..193bc7267 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1233,7 +1233,7 @@ Please restart and report NOW.";
       c#set i
 	s 
 	(fun () -> try_interptac (s ^ ". "))
-	(fun () -> prerr_endline "Clicked")
+	(fun () -> self#insert_command (s^".\n") (s^".\n"))
     in
     set 0 "Assumption" ;
     set 1 "Reflexivity" ;
@@ -1977,7 +1977,8 @@ let main files =
     if analyzed_view#is_active then ignore (f analyzed_view)
   in
   let do_if_active f = do_if_not_computing (do_if_active f) in
-  ignore (tactics_factory#add_item "_Blaster" 
+
+  ignore (tactics_factory#add_item "_Blaster"
 	    ~key:GdkKeysyms._b
 	    ~callback:(do_if_active (fun a -> a#blaster ()))
 	 )