Coqide: use labels for all labelled functions

 This isn't mandatory, but it's a good practice.
 For instance it allows to easily locate all ~callback arguments.
 Cf. warning 6 of OCaml 4

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

3 files changed, 24 insertions, 28 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index f12ea9a24..f244e630f 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -522,10 +522,8 @@ object(self)
       if dir=Down then stop#forward_search else start#backward_search
     in
     match search text with
-      | None -> ()
-      | Some(start, _) ->
-        (b#place_cursor start;
-         self#recenter_insert)
+      |None -> ()
+      |Some(where, _) -> b#place_cursor ~where; self#recenter_insert
 
   method show_goals h k =
     Coq.PrintOpt.set_printing_width proof_view#width;
@@ -1573,7 +1571,7 @@ let coq_icon () =
 
 let about _ =
   let dialog = GWindow.about_dialog () in
-  let _ = dialog#connect#response (fun _ -> dialog#destroy ()) in
+  let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in
   let _ =
     try dialog#set_logo (GdkPixbuf.from_file (coq_icon ()))
     with _ -> ()
@@ -1720,6 +1718,11 @@ let template_item (text, offset, len, key) =
   in
   item name ~label ~callback ~accel:(modifier^key)
 
+let emit_to_focus window sgn =
+  let focussed_widget = GtkWindow.Window.get_focus window#as_window in
+  let obj = Gobject.unsafe_cast focussed_widget in
+  try GtkSignal.emit_unit obj ~sgn with _ -> ()
+
 (** Creation of the main coqide window *)
 
 let build_ui () =
@@ -1737,13 +1740,6 @@ let build_ui () =
   in
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
-  let emit_to_focus sgn =
-    let focussed_widget = GtkWindow.Window.get_focus w#as_window in
-    let obj = Gobject.unsafe_cast focussed_widget in
-    try GtkSignal.emit_unit obj sgn
-    with _ -> ()
-  in
-
   let file_menu = GAction.action_group ~name:"File" () in
   let edit_menu = GAction.action_group ~name:"Edit" () in
   let view_menu = GAction.action_group ~name:"View" () in
@@ -1791,11 +1787,11 @@ let build_ui () =
     item "Redo" ~stock:`REDO
       ~callback:(fun _ -> session_notebook#current_term.script#redo ());
     item "Cut" ~stock:`CUT
-      ~callback:(fun _ -> emit_to_focus GtkText.View.S.cut_clipboard);
+      ~callback:(fun _ -> emit_to_focus w GtkText.View.S.cut_clipboard);
     item "Copy" ~stock:`COPY
-      ~callback:(fun _ -> emit_to_focus GtkText.View.S.copy_clipboard);
+      ~callback:(fun _ -> emit_to_focus w GtkText.View.S.copy_clipboard);
     item "Paste" ~stock:`PASTE
-      ~callback:(fun _ -> emit_to_focus GtkText.View.S.paste_clipboard);
+      ~callback:(fun _ -> emit_to_focus w GtkText.View.S.paste_clipboard);
     item "Find" ~stock:`FIND
       ~callback:(fun _ -> session_notebook#current_term.finder#show `FIND);
     item "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 4f8a3a10f..ad12ad5fd 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1015,7 +1015,7 @@ class configuration_box (tt : GData.tooltips) conf_struct =
 
   let set_icon iter = function
   | None -> ()
-  | Some icon -> tree#set iter icon_col icon
+  | Some icon -> tree#set ~row:iter ~column:icon_col icon
   in
 
   (* Populate the tree *)
@@ -1036,9 +1036,9 @@ class configuration_box (tt : GData.tooltips) conf_struct =
           method apply () = List.iter (fun param -> param#apply) params
         end
       in
-      let () = tree#set new_iter label_col label in
+      let () = tree#set ~row:new_iter ~column:label_col label in
       let () = set_icon new_iter icon in
-      let () = tree#set new_iter box_col widget in
+      let () = tree#set ~row:new_iter ~column:box_col widget in
       ()
     | Section_list (label, icon, struct_list) ->
       let widget =
@@ -1049,9 +1049,9 @@ class configuration_box (tt : GData.tooltips) conf_struct =
           method box = box#coerce
         end
       in
-      let () = tree#set new_iter label_col label in
+      let () = tree#set ~row:new_iter ~column:label_col label in
       let () = set_icon new_iter icon in
-      let () = tree#set new_iter box_col widget in
+      let () = tree#set ~row:new_iter ~column:box_col widget in
       List.iter (make_tree (Some new_iter)) struct_list
   in
 
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index a04c2278c..1628d58d9 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -213,13 +213,13 @@ class finder (view : GText.view) =
 
     initializer
       let _ = self#hide () in
-      let _ = next_button#connect#clicked self#find_forward in
-      let _ = previous_button#connect#clicked self#find_backward in
-      let _ = r_next_button#connect#clicked self#find_forward in
-      let _ = r_previous_button#connect#clicked self#find_backward in
-      let _ = r_replace_button#connect#clicked self#replace in
-      let _ = r_replace_all_button#connect#clicked self#replace_all in
-      ()
+      let _ = next_button#connect#clicked ~callback:self#find_forward in
+      let _ = previous_button#connect#clicked ~callback:self#find_backward in
+      let _ = r_next_button#connect#clicked ~callback:self#find_forward in
+      let _ = r_previous_button#connect#clicked ~callback:self#find_backward in
+      let _ = r_replace_button#connect#clicked ~callback:self#replace in
+      let _ = r_replace_all_button#connect#clicked ~callback:self#replace_all
+      in ()
 
   end
 
@@ -276,7 +276,7 @@ class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.
 
     initializer
       let _ = self#hide () in
-      let _ = next_button#connect#clicked self#search in
+      let _ = next_button#connect#clicked ~callback:self#search in
       ()
 
   end