diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
tree | 9b221c283c2971f7ac151397231059e1d239e723 /ide/coqide_ui.ml | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r-- | ide/coqide_ui.ml | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 0d7c67ac..eaf1e934 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -56,6 +56,22 @@ let init () = <separator /> <menuitem name='Prefs' action='Preferences' /> </menu> + <menu name='View' action='View'> + <menuitem action='Previous tab' /> + <menuitem action='Next tab' /> + <separator/> + <menuitem action='Show Toolbar' /> + <menuitem action='Show Query Pane' /> + <separator/> + <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='Navigation'> <menuitem action='Forward' /> <menuitem action='Backward' /> @@ -100,16 +116,6 @@ let init () = <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' /> @@ -117,8 +123,6 @@ let init () = <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'> |