X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=dc81593c54cddffc035aa0c30bc81e951e8e5d36;hb=2937563e3cfbdccec504dc99b26d64e0b5301c7c;hp=1e2b548267d9f95f31da8221b3c97c81fca90d0b;hpb=a956992315e3a723c69dff5edc361ea3db75cd54;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 1e2b54826..dc81593c5 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -183,8 +183,6 @@ class gui () =
           | false -> self#main#toplevel#unfullscreen ())
         ~check:self#main#fullscreenMenuItem;
       self#main#fullscreenMenuItem#set_active false;
-        (* quit *)
-      self#setQuitCallback (fun () -> exit 0);
         (* log *)
       MatitaLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
@@ -251,6 +249,19 @@ class gui () =
         connect_key self#sourceView#event
           ~modifiers:[`CONTROL] ~stop:true sym f
       in
+        (* quit *)
+      self#setQuitCallback (fun () -> 
+        if 
+          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>")
+            ()
+        then 
+          (saveScript ();prerr_endline "SAVE";GMain.Main.quit ())
+        else
+          GMain.Main.quit ());
       connect_button self#main#scriptAdvanceButton advance;
       connect_button self#main#scriptRetractButton retract;
       connect_button self#main#scriptTopButton top;
@@ -356,8 +367,9 @@ class gui () =
         keyBindingBoxes
 
     method setQuitCallback callback =
-      ignore (main#toplevel#connect#destroy callback);
       ignore (main#quitMenuItem#connect#activate callback);
+      ignore (main#toplevel#event#connect#delete 
+        (fun _ -> callback ();true));
       self#addKeyBinding GdkKeysyms._q callback
 
     method chooseFile ?(ok_not_exists = false) () =