diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
| commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
| tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /ide/utils | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'ide/utils')
| -rw-r--r-- | ide/utils/configwin.ml | 4 | ||||
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml index 3ff60799..4606ef29 100644 --- a/ide/utils/configwin.ml +++ b/ide/utils/configwin.ml @@ -60,9 +60,9 @@ let html = Configwin_ihm.html let edit ?(apply=(fun () -> ())) - title ?(width=400) ?(height=400) + title ?width ?height conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ~width ~height conf_struct_list + Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list let get = Configwin_ihm.edit ~with_apply: false ~apply: (fun () -> ()) diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 9ddc90ef..7dbd0452 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -1022,7 +1022,7 @@ class configuration_box (tt : GData.tooltips) conf_struct = let rec make_tree iter conf_struct = (* box is not shown at first *) - let box = GPack.vbox ~packing:menu_box#add ~show:false () in + let box = GPack.vbox ~packing:(menu_box#pack ~expand:true) ~show:false () in let new_iter = match iter with | None -> tree#append () | Some parent -> tree#append ~parent () @@ -1136,12 +1136,12 @@ let tabbed_box conf_struct_list buttons tooltips = to configure the various parameters. *) let edit ?(with_apply=true) ?(apply=(fun () -> ())) - title ?(width=400) ?(height=400) + title ?width ?height conf_struct = let dialog = GWindow.dialog ~position:`CENTER ~modal: true ~title: title - ~height ~width + ?height ?width () in let tooltips = GData.tooltips () in |