From 9829f5885ee8cecab0ffcfcba5ef558fc976f601 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 11 Jan 2011 22:25:40 +0000
Subject: [PATCH] ctrl+pgUp/Down to navigate tabs

---
 matita/matita/matitaGtkMisc.ml  |  7 -------
 matita/matita/matitaGtkMisc.mli |  2 --
 matita/matita/matitaGui.ml      | 15 ++++++++++-----
 3 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 23b427c5a..aaf297da2 100644
--- a/matita/matita/matitaGtkMisc.ml
+++ b/matita/matita/matitaGtkMisc.ml
@@ -78,13 +78,6 @@ let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () =
 let toggle_callback ~callback ~(check: GMenu.check_menu_item) =
   ignore (check#connect#toggled (fun _ -> callback check#active))
   
-let add_key_binding key callback (evbox: GBin.event_box) =
-  ignore (evbox#event#connect#key_press (function
-    | key' when GdkEvent.Key.keyval key' = key ->
-        callback ();
-        false
-    | _ -> false))
-
 class multiStringListModel ~cols (tree_view: GTree.view) =
   let column_list = new GTree.column_list in
   let text_columns = 
diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli
index 6c10ba664..05a724136 100644
--- a/matita/matita/matitaGtkMisc.mli
+++ b/matita/matita/matitaGtkMisc.mli
@@ -41,8 +41,6 @@ val toggle_callback:
 val toggle_win:
   ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit
 
-val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
-
 (** Connect a callback to the clicked signal of a button, ignoring its return
   * value *)
 val connect_button: #GButton.button -> (unit -> unit) -> unit
diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 99a93773b..f29fb44bc 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -420,14 +420,18 @@ class gui () =
       let s () = MatitaScript.current () in
         (* key bindings *)
       List.iter (* global key bindings *)
-        (fun (key, callback) -> self#addKeyBinding key callback)
+        (fun (key, modifiers, callback) -> 
+                self#addKeyBinding key ~modifiers callback)
 (*
         [ GdkKeysyms._F3,
             toggle_win ~check:main#showProofMenuItem proof#proofWin;
           GdkKeysyms._F4,
             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 *)
-        [ ];
+        [ 
+          GdkKeysyms._Page_Up,   [`CONTROL], main#scriptNotebook#next_page;
+          GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#previous_page
+        ];
         (* about win *)
       let parse_txt_file file =
        let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
@@ -752,7 +756,7 @@ class gui () =
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
         ~callback:(function b ->
           let s = s () in
-          let status = Interpretations.toggle_active_interpretations s#status b
+          let _status = Interpretations.toggle_active_interpretations s#status b
           in
            assert false (* MATITA 1.0 ???
            s#set_grafite_status status*)
@@ -1033,8 +1037,9 @@ class gui () =
     method private findRepl = findRepl
     method main = main
 
-    method private addKeyBinding key callback =
-      List.iter (fun evbox -> add_key_binding key callback evbox)
+    method private addKeyBinding key ?modifiers callback =
+(*       List.iter (fun evbox -> add_key_binding key callback evbox) *)
+      List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback)
         keyBindingBoxes
 
     method private setQuitCallback callback =
-- 
2.39.2