diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:13 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:13 +0000 |
| commit | 8a4315ed0852b4a7559da977d7e2aa3fe939dd79 (patch) | |
| tree | a05731d1989f7c5ee79f111066229c45be904edb /ide/wg_Command.ml | |
| parent | c93c937799c262e65d2c8cbaf3d9f7e60c590039 (diff) | |
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
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 8 |
1 files changed, 5 insertions, 3 deletions
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) |