From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- ide/wg_Command.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'ide/wg_Command.ml') diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 8eddfb31..06281d62 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -98,7 +98,7 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let result = Wg_MessageView.message_view () in router#register_route route_id result; - r_bin#add (result :> GObj.widget); + r_bin#add_with_viewport (result :> GObj.widget); views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in @@ -152,9 +152,9 @@ object(self) method show = frame#show; let cur_page = notebook#get_nth_page notebook#current_page in - let _, _, e = - List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in - e#misc#grab_focus () + match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with + | (_, _, e) -> e#misc#grab_focus () + | exception Not_found -> () method hide = frame#hide -- cgit v1.2.3