diff --git a/src/plugins/gui/debug_manager.ml b/src/plugins/gui/debug_manager.ml index 4d7e45a1d505eca845707c743f67b47296ad77c9..6f8def06cba235523e513618e8921f1f6ab4686b 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 d6cd25ea9dc06578e7d9ee03e6f749e6a423ff10..b7993e453b38bc6cec60730169b6e05e95f7b649 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 761b616153aff9a957548ca7207f9fe055d29a37..28a94e116322e6833d6920a7d5c3a9750008b79a 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 24761d0f03f493a6f77abbf0c2ead3deb7f63bd5..fd8db91cf27e7d23cb4a1da1633d4bf50f488213 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 582ded99e873539e52573aef07d1967472eefb90..0f80fe87c68ee11f53589b74905d4255ee6fae33 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 a4a6d79740dac47aefd89442aecf8584adad557b..57ffc3c620c4d6af6ec240eff2ceee389a09fc93 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 ();