From 8a4315ed0852b4a7559da977d7e2aa3fe939dd79 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Tue, 22 Oct 2013 09:22:13 +0000 Subject: Wg_Commands: fix warning "widget not within a GtkWindow" The constructor was calling indirectly grab_default that requires the widget to be anchored. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_Command.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'ide/wg_Command.ml') diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 8755db372..6c0d1c3ad 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -116,7 +116,9 @@ object(self) notebook#set_page ~tab_label:b#coerce page; new_page <- page - method new_query ?command ?term () = + method new_query ?command ?term () = self#new_query_aux ?command ?term () + + method private new_query_aux ?command ?term ?(grab_now=true) () = let frame = GBin.frame ~shadow_type:`NONE () in ignore(notebook#insert_page ~pos:(notebook#page_num new_page) frame#coerce); let new_tab_lbl text = @@ -196,7 +198,7 @@ object(self) | Some t -> entry#set_text t end; combo#entry#misc#grab_focus (); - entry#misc#grab_default (); + if grab_now then entry#misc#grab_default (); ignore (entry#connect#activate ~callback); ignore (combo#entry#connect#activate ~callback); ignore (combo#entry#event#connect#key_press ~callback:(fun ev -> @@ -228,7 +230,7 @@ object(self) initializer self#new_page_maker; - self#new_query (); + self#new_query_aux ~grab_now:false (); frame#misc#hide (); ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) -- cgit v1.2.3