added "are you sure you want to quit with usaved script?"

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 1e2b548267d9f95f31da8221b3c97c81fca90d0b..dc81593c54cddffc035aa0c30bc81e951e8e5d36 100644 (file)
--- 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) () =