Coqide: GEdit.combo is deprecated since Gtk2.4! We now use GEdit.combo_box_entry_text

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

4 files changed, 42 insertions, 36 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index e42c57abec..739435df4f 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -74,14 +74,10 @@ object(self)
     notebook#goto_page (notebook#page_num frame#coerce);
     let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
     let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
-    let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
-		  ~enable_arrow_keys:true
-		  ~allow_empty:false
-		  ~value_in_list:false (* true is not ok with disable_activate...*)
+    let (combo,_) = GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving
 		  ~packing:hbox#pack
 		  ()
     in
-    combo#disable_activate ();
     let on_activate c () =
       if List.mem combo#entry#text Coq_commands.state_preserving then c ()
       else prerr_endline "Not a state preserving command"
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b2ae010088..94845e21b2 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2609,12 +2609,9 @@ let main files =
     ~packing:(lower_hbox#pack ~expand:false) ()
   in
   let search_history = ref [] in
-  let search_input = GEdit.combo ~popdown_strings:!search_history
-    ~enable_arrow_keys:true
-    ~show:false
+  let (search_input,_) = GEdit.combo_box_entry_text ~strings:!search_history ~show:false
     ~packing:(lower_hbox#pack ~expand:false) ()
   in
-  search_input#disable_activate ();
   let ready_to_wrap_search = ref false in
 
   let start_of_search = ref None in
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c0d46aca57..c9e832bb1d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -520,6 +520,7 @@ let configure ?(apply=(fun () -> ())) () =
     combo
       "Library URL"
       ~f:(fun s -> !current.library_url <- s)
+      ~new_allowed: true
       (predefined@[if List.mem !current.library_url predefined then ""
                    else !current.library_url])
       !current.library_url
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index fefb268259..1eb8f739fa 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -393,38 +393,50 @@ class string_param_box param (tt:GData.tooltips) =
 
 (** This class is used to build a box for a combo parameter.*)
 class combo_param_box param (tt:GData.tooltips) =
-  let _ = dbg "combo_param_box" in
-  let hbox = GPack.hbox () in
-  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
-  let wc = GEdit.combo
-      ~popdown_strings: param.combo_choices
-      ~value_in_list: (not param.combo_new_allowed)
-      (* ~allow_empty: param.combo_blank_allowed *)
-      ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
-      ()
-  in
-  let _ =
-    match param.combo_help with
-      None -> ()
-    | Some help ->
-	tt#set_tip ~text: help ~privat: help wev#coerce
-  in
-  let _ = wc#entry#set_editable param.combo_editable in
-  let _ = wc#entry#set_text param.combo_value in
-
-  object (self)
-    (** This method returns the main box ready to be packed. *)
-    method box = hbox#coerce
+    let _ = dbg "combo_param_box" in
+    let hbox = GPack.hbox () in
+    let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
+    let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
+    let _ =
+      match param.combo_help with
+	  None -> ()
+	| Some help ->
+	    tt#set_tip ~text: help ~privat: help wev#coerce
+    in
+    let get_value = if not param.combo_new_allowed then
+      let wc = GEdit.combo_box_text
+	~strings: param.combo_choices
+	?active:(let rec aux i = function
+		   |[] -> None
+		   |h::_ when h = param.combo_value -> Some i
+		   |_::t -> aux (succ i) t
+		 in aux 0 param.combo_choices)
+	~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+	()
+      in
+	fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
+    else
+      let (wc,_) = GEdit.combo_box_entry_text
+	~strings: param.combo_choices
+	~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+	()
+      in
+      let _ = wc#entry#set_editable param.combo_editable in
+      let _ = wc#entry#set_text param.combo_value in
+	fun () -> wc#entry#text
+    in
+object (self)
+  (** This method returns the main box ready to be packed. *)
+  method box = hbox#coerce
     (** This method applies the new value of the parameter. *)
-    method apply =
-      let new_value = wc#entry#text in
+  method apply =
+    let new_value = get_value () in
       if new_value <> param.combo_value then
 	let _ = param.combo_f_apply new_value in
-	param.combo_value <- new_value
+	  param.combo_value <- new_value
       else
 	()
-  end ;;
+end ;;
 
 (** Class used to pack a custom box. *)
 class custom_param_box param (tt:GData.tooltips) =