From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2013 12:20:15 +0000 (+0000)
Subject: Patch by Paolo Tranquilli. It fixes the following problem: when a new
X-Git-Tag: make_still_working~1197
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ca065f520dec7152df8e094028119515810b434;p=helm.git

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 0ecede622..94e3e751d 100644
--- 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