X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=d009a63f6f43646846a782265bb276743325e708;hb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;hp=f38a278597a51f1dd7fbeaf23d7a97751bbd4271;hpb=364d23cb116e167d3b23f6ef0412830e816e5e92;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index f38a27859..d009a63f6 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -128,15 +128,19 @@ class console ~(buffer: GText.buffer) () =
 let clean_current_baseuri status = 
   LibraryClean.clean_baseuris [status#baseuri]
 
-let save_moo status = 
-  let script = MatitaScript.current () in
+let save_moo0 ~do_clean script status = 
   let baseuri = status#baseuri in
   match script#bos, script#eos with
   | true, _ -> ()
   | _, true ->
      GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
       status
-  | _ -> clean_current_baseuri status 
+  | _ -> if do_clean then clean_current_baseuri status 
+;;
+
+let save_moo status = 
+ let script = MatitaScript.current () in
+  save_moo0 ~do_clean:true script status
 ;;
     
 let ask_unsaved parent filename =
@@ -415,19 +419,24 @@ class gui () =
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
     val mutable _only_directory = false
+    val mutable current_page = 0
       
     initializer
       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_Down, [`CONTROL], main#scriptNotebook#next_page;
+          GdkKeysyms._Page_Up,   [`CONTROL], main#scriptNotebook#previous_page
+        ];
         (* about win *)
       let parse_txt_file file =
        let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
@@ -589,7 +598,7 @@ class gui () =
                match !id with
                | None -> assert false (* a race condition occurred *)
                | Some id ->
-                   (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id));
+                   source_view#source_buffer#misc#disconnect id));
              source_view#source_buffer#place_cursor
               (source_view#source_buffer#get_iter (`OFFSET x'));
         end;
@@ -752,7 +761,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*)
@@ -825,21 +834,13 @@ class gui () =
       connect_menu_item main#newMenuItem self#newScript;
       connect_menu_item main#closeMenuItem self#closeCurrentScript;
       connect_menu_item main#showCoercionsGraphMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Coercions));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions)));
       connect_menu_item main#showHintsDbMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Hints));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints)));
       connect_menu_item main#showTermGrammarMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Grammar));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar)));
       connect_menu_item main#showUnicodeTable
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `TeX));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
         (* debug menu *)
       main#debugMenu#misc#hide ();
         (* HBUGS *)
@@ -862,7 +863,7 @@ class gui () =
       main#hpaneScriptSequent#set_position script_w;
       (* math view handling *)
       connect_menu_item main#newCicBrowserMenuItem (fun () ->
-        ignore(MatitaMathView.cicBrowser ()));
+        ignore(MatitaMathView.cicBrowser None));
       connect_menu_item main#increaseFontSizeMenuItem
         MatitaMisc.increase_font_size;
       connect_menu_item main#decreaseFontSizeMenuItem
@@ -871,9 +872,12 @@ class gui () =
         MatitaMisc.reset_font_size;
       ignore (main#scriptNotebook#connect#switch_page
        (fun page ->
+         let old_script = MatitaScript.at_page current_page in
+         save_moo0 ~do_clean:false old_script old_script#status;
+         current_page <- page;
          let script = MatitaScript.at_page page in
           script#activate;
-          main#saveMenuItem#misc#set_sensitive script#has_name));
+          main#saveMenuItem#misc#set_sensitive script#has_name))
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -978,20 +982,19 @@ class gui () =
     method newScript () = 
        let scrolledWindow = GBin.scrolled_window () in
        let hbox = GPack.hbox () in
-       let tab_label = GMisc.label ~text:"foo"
-        ~packing:hbox#pack () in
+       let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
        let _ =
         GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
        let closebutton =
         GButton.button ~relief:`NONE ~packing:hbox#pack () in
-       let image =
-        GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
+       let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
        closebutton#set_image image#coerce;
        let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
         ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
          scrolledWindow#coerce);
         ignore (closebutton#connect#clicked (fun () ->
-           self#closeScript (main#scriptNotebook#page_num hbox#coerce) script));
+         self#closeScript
+          (main#scriptNotebook#page_num scrolledWindow#coerce) script));
         main#scriptNotebook#goto_page 0;
         sequents_viewer#reset;
         sequents_viewer#load_logo;
@@ -1042,8 +1045,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 =
@@ -1071,8 +1075,10 @@ class gui () =
 
 let gui () = 
   let g = new gui () in
-  MatitaMisc.set_gui g;
-  g
+  let rg = (g :> MatitaGuiTypes.gui) in
+  MatitaMisc.set_gui rg;
+  g#newScript ();
+  rg
   
 let instance = singleton gui