coqide: blaster 2

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

4 files changed, 125 insertions, 46 deletions

diff --git a/.depend b/.depend
index 2d49a1212f..9ff40b6026 100644
--- a/.depend
+++ b/.depend
@@ -476,8 +476,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx 
 doc/parse.cmo: parsing/ast.cmi 
 doc/parse.cmx: parsing/ast.cmx 
-ide/blaster_window.cmo: ide/coq.cmi 
-ide/blaster_window.cmx: ide/coq.cmx 
+ide/blaster_window.cmo: ide/coq.cmi ide/ideutils.cmi 
+ide/blaster_window.cmx: ide/coq.cmx ide/ideutils.cmx 
 ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmi \
     ide/command_windows.cmi 
 ide/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx ide/ideutils.cmx \
diff --git a/Makefile b/Makefile
index 419ccecc1c..82cd79376e 100644
--- a/Makefile
+++ b/Makefile
@@ -386,10 +386,10 @@ COQIDE=bin/coqide$(EXE)
 COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \
 	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
 	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
-	  ide/utils/configwin.cmo ide/blaster_window.cmo \
+	  ide/utils/configwin.cmo \
 	  ide/utils/editable_cells.cmo ide/config_parser.cmo \
 	  ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \
-	  ide/ideutils.cmo ide/undo.cmo \
+	  ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo \
 	  ide/find_phrase.cmo \
           ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
 	  ide/coq_tactics.cmo  ide/command_windows.cmo ide/coqide.cmo
diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
index 32a1c64855..414b86c3bb 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -8,6 +8,9 @@
 
 (* $Id$ *)
 
+open Gobject.Data
+open Ideutils
+
 class blaster_window (n:int) = 
   let window = GWindow.window 
 		 ~allow_grow:true ~allow_shrink:true 
@@ -15,52 +18,125 @@ class blaster_window (n:int) =
 		 ~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 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 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
+  val roots = Hashtbl.create 17
+  val tbl = Hashtbl.create 17
   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 set
+    root
+    name
+    (compute:unit -> Coq.tried_tactic) 
+    (on_click:unit -> unit) 
+    = 
+    let root = 
+      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 name in
+    Hashtbl.add tbl name (nt,compute,on_click)
+
+  method clear () = 
+    model#clear ();      
+    Hashtbl.clear tbl;
+    Hashtbl.clear roots;
 
+      
   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
+    view#expand_all ();
+    Hashtbl.iter 
+      (fun k (nt,compute,on_click) ->
+	 match compute () with 
+	 | Coq.Interrupted -> 
+	     prerr_endline "Interrupted"
+	 | Coq.Failed -> 
+	     prerr_endline "Failed";
+	     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)
+      )
+      tbl
+
   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 -> prerr_endline (GtkTree.TreePath.to_string path);
+		     let it = model#get_iter path in
+		     prerr_endline (string_of_bool (model#iter_is_valid it));
+		     let name = 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 = Hashtbl.find tbl name 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
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 193bc7267e..cbd5c1d118 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1229,21 +1229,23 @@ Please restart and report NOW.";
   method blaster () = 
     prerr_endline "Blaster called";
     let c = Blaster_window.blaster_window () in
+    c#clear ();
     let set i s = 
-      c#set i
+      c#set
+	i
 	s 
 	(fun () -> try_interptac (s ^ ". "))
 	(fun () -> self#insert_command (s^".\n") (s^".\n"))
     in
-    set 0 "Assumption" ;
-    set 1 "Reflexivity" ;
-    set 2 "Trivial";
-    set 3 "Auto" ;
-    set 4 "EAuto";
-    set 5 "Auto with *" ;
-    set 6 "EAuto with *" ;
-    set 7 "Intuition";
-    set 8 "Ground";
+    set "Goal" "Assumption" ;
+    set "Goal" "Reflexivity" ;
+    set "Goal" "Trivial";
+    set "Goal" "Auto" ;
+    set "Goal" "EAuto";
+    set "Goal" "Auto with *" ;
+    set "Goal" "EAuto with *" ;
+    set "Goal" "Intuition";
+    set "Goal" "Ground";
     let _ = Thread.create c#blaster () in
     ()
     
@@ -2209,8 +2211,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   
   (* Command/Compile Menu *)
   let compile_f () =
-    let v = get_active_view () in
+    let v = get_current_view () in
     let av = out_some v.analyzed_view in
+    save_f ();
     match av#filename with
     | None -> 
 	!flash_info "Active buffer has no name"