method set_widths () =
param#wf_elements#misc#set_size_request ~width: elements_frame_width#get ();
param#wf_display#misc#set_size_request ~width:
(match param#display_elt with None -> 0 | Some _ -> display_frame_width#get) () ;
param#wf_output#misc#set_size_request ~height: output_frame_height#get ();