Patch by Paolo Tranquilli. It fixes the following problem: when a new

tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 0ecede6227638f2a6dd304c35704491395d9617a..94e3e751db0f046b2f27cf01f36ca761b8fb202e 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -419,7 +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
+    val mutable current_page = -1
       
     initializer
       let s () = MatitaScript.current () in
@@ -870,14 +870,12 @@ class gui () =
         MatitaMisc.decrease_font_size;
       connect_menu_item main#normalFontSizeMenuItem
         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))
+      ignore (main#scriptNotebook#connect#switch_page (fun page ->
+        self#save_page ();
+        current_page <- page;
+        let script = MatitaScript.at_page page in
+        script#activate;
+        main#saveMenuItem#misc#set_sensitive script#has_name))
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -979,7 +977,13 @@ class gui () =
      let script = MatitaScript.at_page page in 
       self#closeScript page script
 
+    method private save_page () =
+      if current_page >= 0 then
+        let old_script = MatitaScript.at_page current_page in
+        save_moo0 ~do_clean:false old_script old_script#status
+
     method newScript () = 
+       self#save_page ();
        let scrolledWindow = GBin.scrolled_window () in
        let hbox = GPack.hbox () in
        let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in