summaryrefslogtreecommitdiff
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 18:33:25 +0100
commit1b92c226e563643da187b8614d5888dc4855eb43 (patch)
treec4c3d204b36468b58cb71050ba95f06b8dd7bc2e /ide/coqide_ui.ml
parent7c9b0a702976078b813e6493c1284af62a3f093c (diff)
Imported Upstream version 8.6
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index edfe28b2..2ae18593 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -18,6 +18,15 @@ let list_items menu li =
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 = "<menuitem action='"^menu^" "^(no_under q)^"' />\n" in
+ Buffer.add_string res_buf s
+ in
+ let () = List.iter query_item li in
+ res_buf
+
let init () =
let theui = Printf.sprintf "<ui>
<menubar name='CoqIde MenuBar'>
@@ -119,6 +128,8 @@ let init () =
<menuitem action='About' />
<menuitem action='Locate' />
<menuitem action='Print Assumptions' />
+ <separator />
+ %s
</menu>
<menu name='Tools' action='Tools'>
<menuitem action='Comment' />
@@ -162,5 +173,6 @@ let init () =
(if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" 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);