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

2 files changed, 31 insertions, 22 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index dc63de6090..1aa3a70cfb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2330,13 +2330,13 @@ let main files =
   in
 
   let file_actions = GAction.action_group ~name:"File" () in
-  let export_actions = GAction.action_group ~name:"Export" () in
   let edit_actions = GAction.action_group ~name:"Edit" () in
+  let view_actions = GAction.action_group ~name:"View" () in
+  let export_actions = GAction.action_group ~name:"Export" () in
   let navigation_actions = GAction.action_group ~name:"Navigation" () in
   let tactics_actions = GAction.action_group ~name:"Tactics" () in
   let templates_actions = GAction.action_group ~name:"Templates" () in
   let queries_actions = GAction.action_group ~name:"Queries" () in
-  let display_actions = GAction.action_group ~name:"Display" () in
   let compile_actions = GAction.action_group ~name:"Compile" () in
   let windows_actions = GAction.action_group ~name:"Windows" () in
   let help_actions = GAction.action_group ~name:"Help" () in
@@ -2453,6 +2453,21 @@ let main files =
 	end;
 	reset_revert_timer ()) ~stock:`PREFERENCES;
       (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
+    GAction.add_actions view_actions [
+      GAction.add_action "View" ~label:"_View";
+      GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<SHIFT>Left") ~stock:`GO_BACK
+        ~callback:(fun _ -> session_notebook#previous_page ());
+      GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD
+        ~callback:(fun _ -> session_notebook#next_page ());
+    ];
+    List.iter
+      (fun (opts,name,label,key,dflt) ->
+         GAction.add_toggle_action name ~active:dflt ~label
+           ~accel:(!current.modifier_for_display^key)
+          ~callback:(fun v -> do_or_activate (fun a ->
+            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
+            a#show_goals) ()) view_actions)
+      print_items;
     GAction.add_actions navigation_actions [
       GAction.add_action "Navigation" ~label:"_Navigation";
       GAction.add_action "Forward" ~label:"_Forward" ~stock:`GO_DOWN
@@ -2535,15 +2550,6 @@ let main files =
       query_shortcut "Locate" None;
       query_shortcut "Whelp Locate" None;
     ];
-    GAction.add_action "Display" ~label:"_Display" display_actions;
-    List.iter
-      (fun (opts,name,label,key,dflt) ->
-         GAction.add_toggle_action name ~active:dflt ~label
-	   ~accel:(!current.modifier_for_display^key)
-          ~callback:(fun v -> do_or_activate (fun a ->
-            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
-            a#show_goals) ()) display_actions)
-      print_items;
     GAction.add_actions compile_actions [
       GAction.add_action "Compile" ~label:"_Compile";
       GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f;
@@ -2611,11 +2617,11 @@ let main files =
     Coqide_ui.ui_m#insert_action_group file_actions 0;
     Coqide_ui.ui_m#insert_action_group export_actions 0;
     Coqide_ui.ui_m#insert_action_group edit_actions 0;
+    Coqide_ui.ui_m#insert_action_group view_actions 0;
     Coqide_ui.ui_m#insert_action_group navigation_actions 0;
     Coqide_ui.ui_m#insert_action_group tactics_actions 0;
     Coqide_ui.ui_m#insert_action_group templates_actions 0;
     Coqide_ui.ui_m#insert_action_group queries_actions 0;
-    Coqide_ui.ui_m#insert_action_group display_actions 0;
     Coqide_ui.ui_m#insert_action_group compile_actions 0;
     Coqide_ui.ui_m#insert_action_group windows_actions 0;
     Coqide_ui.ui_m#insert_action_group help_actions 0;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 0d7c67acf0..a29197486a 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' />