From 4d692708fbd3011187c1db7ff7df302686c68ff3 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 3 Jan 2019 15:03:42 +0100 Subject: [PATCH] [gui] get rid of deprecated (and removed in gtk3) attributes allow_{shrink,grow} --- src/plugins/gui/debug_manager.ml | 4 +--- src/plugins/gui/design.ml | 5 +---- src/plugins/gui/gtk_helper.ml | 4 ++-- src/plugins/gui/launcher.ml | 3 +-- src/plugins/gui/wpane.ml | 2 +- src/plugins/impact/register_gui.ml | 4 +--- 6 files changed, 7 insertions(+), 15 deletions(-) diff --git a/src/plugins/gui/debug_manager.ml b/src/plugins/gui/debug_manager.ml index 4d7e45a1d50..6f8def06cba 100644 --- a/src/plugins/gui/debug_manager.ml +++ b/src/plugins/gui/debug_manager.ml @@ -49,9 +49,7 @@ let graph_window main_window title mk_view = let height = int_of_float (float main_window#default_height *. 3. /. 4.) in let width = int_of_float (float main_window#default_width *. 3. /. 4.) in let window = - GWindow.window - ~width ~height ~title ~allow_shrink:true ~allow_grow:true - ~position:`CENTER () + GWindow.window ~width ~height ~title ~resizable:true ~position:`CENTER () in let view = mk_view ~packing:window#add () in window#show (); diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml index d6cd25ea9dc..b7993e453b3 100644 --- a/src/plugins/gui/design.ml +++ b/src/plugins/gui/design.ml @@ -847,10 +847,7 @@ class main_window () : main_window_extension_points = ~width ~height ~position:`CENTER -(*GTK3: arguments do not exist anymore at GTK level. *) -(* ~allow_shrink:true - ~allow_grow:true -*) + ~resizable:true ~show:false () in diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml index 761b616153a..28a94e11632 100644 --- a/src/plugins/gui/gtk_helper.ml +++ b/src/plugins/gui/gtk_helper.ml @@ -988,8 +988,8 @@ let graph_window ~parent ~title make_view = let width = int_of_float (float parent#default_width *. 3. /. 4.) in let graph_window = GWindow.window - ~width ~height ~title ~allow_shrink:true ~allow_grow:true - ~position:`CENTER () in + ~width ~height ~title ~resizable:true ~position:`CENTER () + in let view = make_view ~packing:graph_window#add () in graph_window#show(); view#adapt_zoom(); diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml index 24761d0f03f..fd8db91cf27 100644 --- a/src/plugins/gui/launcher.ml +++ b/src/plugins/gui/launcher.ml @@ -253,11 +253,10 @@ let show ?height ?width ~(host:basic_main) () = ~title:"Launching analysis" ~modal:true ~position:`CENTER_ON_PARENT - ~allow_shrink:true + ~resizable:true ?width ?height ~parent:host#main_window - ~allow_grow:true () in ignore (dialog#misc#connect#size_allocate diff --git a/src/plugins/gui/wpane.ml b/src/plugins/gui/wpane.ml index 582ded99e87..0f80fe87c68 100644 --- a/src/plugins/gui/wpane.ml +++ b/src/plugins/gui/wpane.ml @@ -217,7 +217,7 @@ class ['a] dialog ~title ~window ?(resize=false) () = let shell = GWindow.window ~title ~kind:`TOPLEVEL ~modal:true ~show:false ~decorated:true ~position:`CENTER_ON_PARENT - ~allow_grow:resize () + ~resizable:resize () in let hclip = GBin.alignment ~packing:shell#add () in diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml index a4a6d79740d..57ffc3c620c 100644 --- a/src/plugins/impact/register_gui.ml +++ b/src/plugins/impact/register_gui.ml @@ -167,9 +167,7 @@ let reason_graph_window main_window ?in_kf reason = let height = int_of_float (float main_window#default_height *. 3. /. 4.) in let width = int_of_float (float main_window#default_width *. 3. /. 4.) in let window = - GWindow.window - ~width ~height ~allow_shrink:true ~allow_grow:true - ~position:`CENTER () + GWindow.window ~width ~height ~resizable:true ~position:`CENTER () in let view = reason_graph ~packing:window#add in window#show (); -- GitLab