summaryrefslogtreecommitdiff
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml151
1 files changed, 151 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
new file mode 100644
index 00000000..0d7c67ac
--- /dev/null
+++ b/ide/coqide_ui.ml
@@ -0,0 +1,151 @@
+let ui_m = GAction.ui_manager ();;
+
+let no_under = Minilib.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 ("<menuitem action='"^menu^" "^(no_under s)^"' />\n") in
+ b
+ |s::_ as l -> let b = Buffer.create 50 in
+ let () = (Buffer.add_string b ("<menu action='"^menu^" "^(String.make 1 s.[0])^"'>\n")) in
+ let () = (List.iter
+ (fun x -> Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under x)^"' />\n")) l) in
+ let () = Buffer.add_string b"</menu>\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 "<ui>
+<menubar name='CoqIde MenuBar'>
+ <menu action='File'>
+ <menuitem action='New' />
+ <menuitem action='Open' />
+ <menuitem action='Save' />
+ <menuitem action='Save as' />
+ <menuitem action='Save all' />
+ <menuitem action='Revert all buffers' />
+ <menuitem action='Close buffer' />
+ <menuitem action='Print...' />
+ <menu action='Export to'>
+ <menuitem action='Html' />
+ <menuitem action='Latex' />
+ <menuitem action='Dvi' />
+ <menuitem action='Pdf' />
+ <menuitem action='Ps' />
+ </menu>
+ <menuitem action='Rehighlight' />
+ %s
+ </menu>
+ <menu name='Edit' action='Edit'>
+ <menuitem action='Undo' />
+ <menuitem action='Clear Undo Stack' />
+ <separator />
+ <menuitem action='Cut' />
+ <menuitem action='Copy' />
+ <menuitem action='Paste' />
+ <separator />
+ <menuitem action='Find in buffer' />
+ <menuitem action='Find backwards' />
+ <menuitem action='Complete Word' />
+ <separator />
+ <menuitem action='External editor' />
+ <separator />
+ <menuitem name='Prefs' action='Preferences' />
+ </menu>
+ <menu action='Navigation'>
+ <menuitem action='Forward' />
+ <menuitem action='Backward' />
+ <menuitem action='Go to' />
+ <menuitem action='Start' />
+ <menuitem action='End' />
+ <menuitem action='Interrupt' />
+ <menuitem action='Hide' />
+ <menuitem action='Previous' />
+ <menuitem action='Next' />
+ </menu>
+ <menu action='Try Tactics'>
+ <menuitem action='auto' />
+ <menuitem action='auto with *' />
+ <menuitem action='eauto' />
+ <menuitem action='eauto with *' />
+ <menuitem action='intuition' />
+ <menuitem action='omega' />
+ <menuitem action='simpl' />
+ <menuitem action='tauto' />
+ <menuitem action='trivial' />
+ <menuitem action='Wizard' />
+ <separator />
+ %s
+ </menu>
+ <menu action='Templates'>
+ <menuitem action='Lemma' />
+ <menuitem action='Theorem' />
+ <menuitem action='Definition' />
+ <menuitem action='Inductive' />
+ <menuitem action='Fixpoint' />
+ <menuitem action='Scheme' />
+ <menuitem action='match' />
+ <separator />
+ %s
+ </menu>
+ <menu action='Queries'>
+ <menuitem action='SearchAbout' />
+ <menuitem action='Check' />
+ <menuitem action='Print' />
+ <menuitem action='About' />
+ <menuitem action='Locate' />
+ <menuitem action='Whelp Locate' />
+ </menu>
+ <menu action='Display'>
+ <menuitem action='Display implicit arguments' />
+ <menuitem action='Display coercions' />
+ <menuitem action='Display raw matching expressions' />
+ <menuitem action='Display notations' />
+ <menuitem action='Display all basic low-level contents' />
+ <menuitem action='Display existential variable instances' />
+ <menuitem action='Display universe levels' />
+ <menuitem action='Display all low-level contents' />
+ </menu>
+ <menu action='Compile'>
+ <menuitem action='Compile buffer' />
+ <menuitem action='Make' />
+ <menuitem action='Next error' />
+ <menuitem action='Make makefile' />
+ </menu>
+ <menu action='Windows'>
+ <menuitem action='Show/Hide Query Pane' />
+ <menuitem action='Show/Hide Toolbar' />
+ <menuitem action='Detach View' />
+ </menu>
+ <menu name='Help' action='Help'>
+ <menuitem action='Browse Coq Manual' />
+ <menuitem action='Browse Coq Library' />
+ <menuitem action='Help for keyword' />
+ <separator />
+ <menuitem name='Abt' action='About Coq' />
+ </menu>
+</menubar>
+<toolbar name='CoqIde ToolBar'>
+ <toolitem action='Save' />
+ <toolitem action='Close buffer' />
+ <toolitem action='Forward' />
+ <toolitem action='Backward' />
+ <toolitem action='Go to' />
+ <toolitem action='Start' />
+ <toolitem action='End' />
+ <toolitem action='Interrupt' />
+ <toolitem action='Hide' />
+ <toolitem action='Previous' />
+ <toolitem action='Next' />
+ <toolitem action='Wizard' />
+</toolbar>
+</ui>"
+ (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))
+ in
+ ignore (ui_m#add_ui_from_string theui);