X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=c9b387178bc8cd1c780de9940d481013a1d035a0;hb=e67aacd065c5f2bb90dc6b07850b4f4c2bc865fc;hp=dc81593c54cddffc035aa0c30bc81e951e8e5d36;hpb=030d34e0dc025b94d7f0459eff0a84e2ac108b73;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index dc81593c5..c9b387178 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -186,9 +186,7 @@ class gui () =
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
- MatitaLog.error
- (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+ (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
@@ -251,17 +249,23 @@ class gui () =
in
(* quit *)
self#setQuitCallback (fun () ->
- if
- MatitaGtkMisc.ask_confirmation
- ~parent:main#toplevel
- ~title:"Unsaved work!"
- ~message:("Your work is unsaved!\n\n"^
- "Do you want to save the script before exiting?")
- ()
- then
- (saveScript ();prerr_endline "SAVE";GMain.Main.quit ())
- else
- GMain.Main.quit ());
+ if source_view#buffer#modified then
+ begin
+ let rc =
+ MatitaGtkMisc.ask_confirmation
+ ~parent:main#toplevel
+ ~title:"Unsaved work!"
+ ~message:("Your work is unsaved!\n\n"^
+ "Do you want to save the script before exiting?")
+ ()
+ 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 ());
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;