coqide: toolbar/autosave

Hugo: Suppression du type dans les notations == et <> entre
Suppression du type dans les notations == et <> entre
volution second traducteur selon discussion  TYPES


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

2 files changed, 98 insertions, 14 deletions

diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 04d7c05ede..d01b830030 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1059,16 +1059,19 @@ let edit ?(with_apply=true)
 
   let hbox_buttons = GPack.hbox ~packing: (vbox#pack ~expand: false ~padding: 4) () in
   let bApply = GButton.button
-      ~label: Configwin_messages.mApply
-      ()
+		 ~stock:`APPLY
+		 ~label: Configwin_messages.mApply
+		 ()
   in
   if with_apply then hbox_buttons#pack ~expand: true ~padding: 3 bApply#coerce;
   let bOk = GButton.button
+	      ~stock:`OK
       ~label: Configwin_messages.mOk
       ~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
       ()
   in
   let bCancel = GButton.button
+		  ~stock:`CANCEL
       ~label: Configwin_messages.mCancel
       ~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
       ()
@@ -1091,6 +1094,9 @@ let edit ?(with_apply=true)
   let f_cancel () = window#destroy () in
   let _ = bCancel#connect#clicked f_cancel in
 
+  let _ = window#event#connect#key_press ~callback:
+	    (fun k -> if GdkEvent.Key.keyval k = GdkKeysyms._Escape then f_cancel ();false)
+  in
   let _ = window#show () in
   GMain.Main.main () ;
   !return
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 1fd15f77aa..20111bf84a 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -3,11 +3,17 @@ open Gobject
 
 let create l = 
   let hbox = GPack.hbox () in
+  let scw = GBin.scrolled_window 
+	      ~hpolicy:`AUTOMATIC 
+	      ~vpolicy:`AUTOMATIC 
+	      ~packing:(hbox#pack ~expand:true) () in
+
   let columns = new GTree.column_list in
   let command_col =  columns#add Data.string in
   let coq_col = columns#add Data.string in
   let store = GTree.list_store columns
   in 
+
 (* populate the store *)
   let _ = List.iter (fun (x,y) -> 
 		       let row = store#append () in
@@ -15,25 +21,97 @@ let create l =
 		       store#set ~row ~column:coq_col y)
 	    l
   in
-  let view = GTree.view ~model:store ~packing:hbox#pack () in
-  
-  let renderer = GTree.cell_renderer_text () in
-  GtkText.Tag.set_property renderer (`EDITABLE true);
+  let view = GTree.view ~model:store ~packing:scw#add_with_viewport () in
+
+  (* Alternate colors for the rows *)
+  view#set_rules_hint true;
+
+  let renderer_comm = GTree.cell_renderer_text () in
+  ignore (GtkSignal.connect renderer_comm 
+	    ~sgn:GtkTree.CellRendererText.Signals.edited 
+	    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
+			 store#set 
+			 ~row:(store#get_iter path) 
+			 ~column:command_col s));
+  GtkText.Tag.set_property renderer_comm (`EDITABLE true);
   let first = 
     GTree.view_column ~title:"Coq Command to try" 
-      ~renderer:(renderer,["text",command_col]) 
+      ~renderer:(renderer_comm,["text",command_col]) 
       () 
   in ignore (view#append_column first);
+
+  let renderer_coq = GTree.cell_renderer_text () in
+  ignore (GtkSignal.connect renderer_coq ~sgn:GtkTree.CellRendererText.Signals.edited 
+    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
+		 store#set 
+		 ~row:(store#get_iter path) 
+		 ~column:coq_col s));
+  GtkText.Tag.set_property renderer_coq (`EDITABLE true);
   let second = 
     GTree.view_column ~title:"Coq Command to insert" 
-      ~renderer:(renderer,["text",coq_col]) 
+      ~renderer:(renderer_coq,["text",coq_col]) 
       () 
   in ignore (view#append_column second);
 
-  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack () in
-  let up = GButton.button ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  let down = GButton.button ~label:"Down" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  let add = GButton.button ~label:"Add" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  let remove = GButton.button ~label:"Remove" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  hbox
+  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () 
+  in
+  let up = GButton.button  ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+  let down = GButton.button 
+	       ~stock:`GO_DOWN 
+	       ~label:"Down" 
+	       ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  in
+  let add = GButton.button ~stock:`ADD 
+	      ~label:"Add" 
+	      ~packing:(vbox#pack ~expand:true ~fill:false) 
+	      () 
+  in
+  let remove = GButton.button ~stock:`REMOVE 
+		 ~label:"Remove" 
+		 ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  in
+
+  ignore (add#connect#clicked 
+	    ~callback:(fun b ->  
+			 let n = store#append () in
+			 view#selection#select_iter n));
+  ignore (remove#connect#clicked 
+	    ~callback:(fun b -> match view#selection#get_selected_rows with 
+			 | [] -> ()
+			 | path::_ ->
+			     let iter = store#get_iter path in
+		       	     ignore (store#remove iter);
+		      ));
+  ignore (up#connect#clicked 
+	    ~callback:(fun b ->  
+			 match view#selection#get_selected_rows with 
+			   | [] -> ()
+			   | path::_ ->
+			       let iter = store#get_iter path in
+			       GtkTree.TreePath.prev path;
+			       let upiter = store#get_iter path in
+			       ignore (store#swap iter upiter);
+		      ));
+  ignore (down#connect#clicked 
+	    ~callback:(fun b ->  
+			 match view#selection#get_selected_rows with 
+			   | [] -> ()
+			   | path::_ ->
+			       let iter = store#get_iter path in
+			       GtkTree.TreePath.next path;
+			       try let upiter = store#get_iter path in
+			       ignore (store#swap iter upiter)
+			       with _ -> ()
+		      ));
+  let get_data () = 
+    let start_path = GtkTree.TreePath.from_string "0" in
+    let start_iter = store#get_iter start_path in
+    let rec all acc = 
+      let new_acc = (store#get ~row:start_iter ~column:command_col,
+		     store#get ~row:start_iter ~column:coq_col)::acc
+      in      
+      if store#iter_next start_iter then all new_acc else List.rev new_acc
+    in all []
+  in
+  (hbox,get_data)