method set_view_interface gvopt =
menuEdit#remove_submenu ();
let menu = GMenu.menu ~packing: menuEdit#set_submenu () in
let l =
match gvopt with
None -> [false; false; false]
| Some gv -> [gv#save <> None; gv#save_as <> None; gv#reload <> None]
in
List.iter2 (fun mi b -> mi#misc#set_sensitive b)
[item_save;item_save_as;item_reload] l;
let l =
match gvopt with
None -> [None;None;None]
| Some gv -> [gv#paste;gv#copy;gv#cut]
in
List.iter2
(fun label fopt ->
let mi = GMenu.menu_item ~packing:menu#append ~label () in
match fopt with
None -> mi#misc#set_sensitive false
| Some f ->
ignore(mi#connect#activate f)
)
["Paste";"Copy";"Cut"]
l;
let mb = viewmenubar in
List.iter mb#remove mb#children;
let f (label,entries) =
let mi = GMenu.menu_item ~label ~packing: (mb#insert ~pos: 0) () in
let mn = GMenu.menu ~packing: mi#set_submenu () in
GToolbox.build_menu mn ~entries
in
match gvopt with
None -> ()
| Some gv -> List.iter f (List.rev gv#menus)