diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-18 14:35:25 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-18 14:35:25 +0000 |
commit | 01c38ee80ef643f5ec85d4bc78bcf4dd16a96e3f (patch) | |
tree | 4886ecbe02ceae9792b7ccf677d1c0089a24ee3e /ide/coqide_ui.ml | |
parent | 03cbf5db1204bc374c1f39c259f10d43031c18b2 (diff) |
Added a tab changing command in CoqIDE and moved display options around
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15200 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r-- | ide/coqide_ui.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 0d7c67acf..a29197486 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -56,6 +56,19 @@ 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='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 +113,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' /> |