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 list_queries menu li =
let res_buf = Buffer.create 500 in
let query_item (q, _) =
let s = "\n" in
Buffer.add_string res_buf s
in
let () = List.iter query_item li in
res_buf
let init () =
let theui = Printf.sprintf "\
\n\
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n\
\n\
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n \
\n\
\n"
(if Coq_config.gtk_platform <> `QUARTZ then "" else "")
(Buffer.contents (list_items "Tactic" Coq_commands.tactics))
(Buffer.contents (list_items "Template" Coq_commands.commands))
(Buffer.contents (list_queries "User-Query" Preferences.user_queries#get))
in
ignore (ui_m#add_ui_from_string theui);