X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=d009a63f6f43646846a782265bb276743325e708;hb=04cd2181640b3828b3d193a8e819c849ef574236;hp=f29fb44bcf19080d9d6de03c7aae40278aafea58;hpb=9829f5885ee8cecab0ffcfcba5ef558fc976f601;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index f29fb44bc..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,6 +419,7 @@ 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
@@ -429,8 +434,8 @@ class gui () =
             toggle_win ~check:main#showCheckMenuItem check#checkWin;
 *)
         [ 
-          GdkKeysyms._Page_Up,   [`CONTROL], main#scriptNotebook#next_page;
-          GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#previous_page
+          GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page;
+          GdkKeysyms._Page_Up,   [`CONTROL], main#scriptNotebook#previous_page
         ];
         (* about win *)
       let parse_txt_file file =
@@ -867,6 +872,9 @@ 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))