let ui_m = GAction.ui_manager ();; let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) let list_items menu li = let res_buf = Buffer.create 500 in let tactic_item = function |[] -> Buffer.create 1 |[s] -> let b = Buffer.create 16 in let () = Buffer.add_string b ("\n") in b |s::_ as l -> let b = Buffer.create 50 in let () = (Buffer.add_string b ("
\n" in b in let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in res_buf let init () = let theui = Printf.sprintf "