avoid losing work on CTRL-N

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index d4157677feabd3573bae00edf5c4d84d52795c3d..589da7dcc8e9adb6eed32d161a7b9b583ec23b33 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -102,7 +102,7 @@ let ask_unsaved parent =
   MatitaGtkMisc.ask_confirmation 
     ~parent ~title:"Unsaved work!" 
     ~message:("Your work is <b>unsaved</b>!\n\n"^
-         "<i>Do you want to save the script before exiting?</i>")
+         "<i>Do you want to save the script before continuing?</i>")
     ()
 
 class gui () =
@@ -605,34 +605,36 @@ class gui () =
               (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
+      let abandon_script () =
+        let status = (s ())#status in
+        if source_view#buffer#modified then
+          (match ask_unsaved main#toplevel with
+          | `YES -> saveScript ()
+          | `NO -> ()
+          | `CANCEL -> raise MatitaTypes.Cancel);
+        (match script_fname with
+        | None -> ()
+        | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+      in
       let loadScript () =
         let script = s () in 
         let status = script#status in
         try 
           match self#chooseFile () with
           | Some f -> 
-                if source_view#buffer#modified then
-                  begin
-                    match ask_unsaved main#toplevel with
-                    | `YES -> saveScript ()
-                    | `NO -> ()
-                    | `CANCEL -> raise MatitaTypes.Cancel
-                  end;
-                (match script_fname with
-                | None -> ()
-                | Some fname -> 
-                    ask_and_save_moo_if_needed main#toplevel fname status);
-                script#reset (); 
-                script#assignFileName f;
-                source_view#source_buffer#begin_not_undoable_action ();
-                script#loadFromFile f; 
-                source_view#source_buffer#end_not_undoable_action ();
-                console#message ("'"^f^"' loaded.\n");
-                self#_enableSaveTo f
+              abandon_script ();
+              script#reset (); 
+              script#assignFileName f;
+              source_view#source_buffer#begin_not_undoable_action ();
+              script#loadFromFile f; 
+              source_view#source_buffer#end_not_undoable_action ();
+              console#message ("'"^f^"' loaded.\n");
+              self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        abandon_script ();
         source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template ();