summaryrefslogtreecommitdiff
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /ide/coqide_ui.ml
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml28
1 files changed, 20 insertions, 8 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index eaf1e934..af71b1e7 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -1,6 +1,6 @@
let ui_m = GAction.ui_manager ();;
-let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x)
+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
@@ -42,14 +42,15 @@ let init () =
</menu>
<menu name='Edit' action='Edit'>
<menuitem action='Undo' />
- <menuitem action='Clear Undo Stack' />
+ <menuitem action='Redo' />
<separator />
<menuitem action='Cut' />
<menuitem action='Copy' />
<menuitem action='Paste' />
<separator />
- <menuitem action='Find in buffer' />
- <menuitem action='Find backwards' />
+ <menuitem action='Find' />
+ <menuitem action='Find Next' />
+ <menuitem action='Find Previous' />
<menuitem action='Complete Word' />
<separator />
<menuitem action='External editor' />
@@ -60,8 +61,12 @@ let init () =
<menuitem action='Previous tab' />
<menuitem action='Next tab' />
<separator/>
+ <menuitem action='Zoom in' />
+ <menuitem action='Zoom out' />
+ <menuitem action='Zoom fit' />
+ <separator/>
<menuitem action='Show Toolbar' />
- <menuitem action='Show Query Pane' />
+ <menuitem action='Query Pane' />
<separator/>
<menuitem action='Display implicit arguments' />
<menuitem action='Display coercions' />
@@ -79,7 +84,6 @@ let init () =
<menuitem action='Start' />
<menuitem action='End' />
<menuitem action='Interrupt' />
- <menuitem action='Hide' />
<menuitem action='Previous' />
<menuitem action='Next' />
</menu>
@@ -109,13 +113,20 @@ let init () =
%s
</menu>
<menu action='Queries'>
- <menuitem action='SearchAbout' />
+ <menuitem action='Search' />
<menuitem action='Check' />
<menuitem action='Print' />
<menuitem action='About' />
<menuitem action='Locate' />
+ <menuitem action='Print Assumptions' />
<menuitem action='Whelp Locate' />
</menu>
+ <menu name='Tools' action='Tools'>
+ <menuitem action='Comment' />
+ <menuitem action='Uncomment' />
+ <separator />
+ <menuitem action='Coqtop arguments' />
+ </menu>
<menu action='Compile'>
<menuitem action='Compile buffer' />
<menuitem action='Make' />
@@ -129,6 +140,7 @@ let init () =
<menuitem action='Browse Coq Manual' />
<menuitem action='Browse Coq Library' />
<menuitem action='Help for keyword' />
+ <menuitem action='Help for μPG mode' />
<separator />
<menuitem name='Abt' action='About Coq' />
</menu>
@@ -141,8 +153,8 @@ let init () =
<toolitem action='Go to' />
<toolitem action='Start' />
<toolitem action='End' />
+ <toolitem action='Force' />
<toolitem action='Interrupt' />
- <toolitem action='Hide' />
<toolitem action='Previous' />
<toolitem action='Next' />
<toolitem action='Wizard' />