matita now asks to save .moo if possible or cleans the dust the

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5ac24f8f66c9abdd262e6f477dd368188edc01e9..7b73eb112b5b2c5f517711da398f67ec1ca82054 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -58,6 +58,50 @@ class console ~(buffer: GText.buffer) () =
       | `Message -> self#message (s ^ "\n")
       | `Warning -> self#warning (s ^ "\n")
   end
+        
+let clean_current_baseuri status = 
+    try  
+      let baseuri = MatitaTypes.get_string_option status "baseuri" in
+      MatitacleanLib.clean_baseuris [baseuri]
+    with MatitaTypes.Option_error _ -> ()
+
+let ask_and_save_moo_if_needed parent fname status = 
+  let save () =
+    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
+  in
+  if (MatitaScript.instance ())#eos then
+    begin
+      let mooname = 
+        MatitaMisc.obj_file_of_script fname
+      in
+      let rc = 
+        MatitaGtkMisc.ask_confirmation
+        ~title:"A .moo can be generated"
+        ~message:(Printf.sprintf 
+          "%s can be generated for %s.\n<i>Should I generate it?</i>"
+          mooname fname)
+        ~parent ()
+      in
+      let b = 
+        match rc with 
+        | `YES -> true 
+        | `NO -> false 
+        | `CANCEL -> raise MatitaTypes.Cancel 
+      in
+      if b then
+        save ()
+      else
+        clean_current_baseuri status
+    end
+  else
+    clean_current_baseuri status 
+    
+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>")
+    ()
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)
@@ -202,17 +246,6 @@ class gui () =
         script_fname <- None;
         self#main#saveMenuItem#misc#set_sensitive false
       in
-      let loadScript () =
-        let script = s () in
-        match self#chooseFile () with
-        | Some f -> 
-              script#reset (); 
-              script#assignFileName f;
-              script#loadFromFile (); 
-              console#message ("'"^f^"' loaded.\n");
-              self#_enableSaveTo f
-        | None -> ()
-      in
       let saveAsScript () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
@@ -231,6 +264,31 @@ class gui () =
               (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
+      let loadScript () =
+        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 -> 
+                script#reset (); 
+                script#assignFileName f;
+                script#loadFromFile (); 
+                console#message ("'"^f^"' loaded.\n");
+                self#_enableSaveTo f
+          | None -> ()
+        with MatitaTypes.Cancel -> ()
+      in
       let newScript () = (s ())#reset (); disableSave () in
       let cursor () =
         source_buffer#place_cursor
@@ -249,23 +307,36 @@ class gui () =
       in
         (* quit *)
       self#setQuitCallback (fun () -> 
+        let status = (MatitaScript.instance ())#status in
         if source_view#buffer#modified then
           begin
-            let rc =  
-              MatitaGtkMisc.ask_confirmation 
-                ~parent:main#toplevel
-                ~title:"Unsaved work!" 
-                ~message:("Your work is <b>unsaved</b>!\n\n"^
-                     "<i>Do you want to save the script before exiting?</i>")
-                ()
-            in
-            match rc with
-            | `YES -> saveScript ();
-                      if not source_view#buffer#modified then
-                        GMain.Main.quit ()
-            | `NO -> GMain.Main.quit ()
-            | `CANCEL -> ()
-          end else GMain.Main.quit ());
+            let rc = ask_unsaved main#toplevel in 
+            try
+              match rc with
+              | `YES -> saveScript ();
+                        if not source_view#buffer#modified then
+                          begin
+                            (match script_fname with
+                            | None -> ()
+                            | Some fname -> 
+                               ask_and_save_moo_if_needed 
+                                 main#toplevel fname status);
+                          GMain.Main.quit ()
+                          end
+              | `NO -> GMain.Main.quit ()
+              | `CANCEL -> raise MatitaTypes.Cancel
+            with MatitaTypes.Cancel -> ()
+          end 
+        else 
+          begin  
+            (match script_fname with
+            | None -> clean_current_baseuri status 
+            | Some fname ->
+                try
+                  ask_and_save_moo_if_needed main#toplevel fname status;
+                  GMain.Main.quit ()
+                with MatitaTypes.Cancel -> ())
+          end);
       connect_button self#main#scriptAdvanceButton advance;
       connect_button self#main#scriptRetractButton retract;
       connect_button self#main#scriptTopButton top;