bugfixes:

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 153d474abe09b6a5e22baff307ebcaac3cc0283a..1b46c03a4e2ea4b678564b503ad21fa35b889cf0 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -606,19 +606,19 @@ class gui () =
         let script = s () in 
         let status = script#status in
         try 
-          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);
           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 ();