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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index d45452a5235176e88a3d27f43cc609d9ebee6b96..b53bbd209dad6ee860c48be855d699fe4036a835 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -23,6 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
+exception PopupClosed
 open Printf
 
 open MatitaTypes
@@ -166,24 +167,51 @@ class type gui =
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
-let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () =
-  let dialog = gui#newConfirmationDialog () in
-  dialog#confirmationDialog#set_title title;
-  dialog#confirmationDialogLabel#set_label msg;
-  let result = ref None in
-  let return r _ =
-    result := Some r;
-    dialog#confirmationDialog#destroy ();
-    GMain.Main.quit ()
+let popup_message 
+  ~title ~message ~buttons ~callback
+  ?(message_type=`QUESTION) ?parent ?(use_markup=true)
+  ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false)
+  ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
+  ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width 
+  ?height ?(show=true) ()
+=
+  let m = 
+    GWindow.message_dialog 
+      ~message ~use_markup ~message_type ~buttons ?parent ~destroy_with_parent 
+      ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen 
+      ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height 
+      ~show () 
+  in 
+  ignore(m#connect#response 
+    ~callback:(fun a ->  GMain.Main.quit ();callback a));
+  ignore(m#connect#close 
+    ~callback:(fun _ -> GMain.Main.quit ();raise PopupClosed));
+  GtkThread.main ()
+
+
+let ask_confirmation ~title ~message ?parent () =
+  let rc = ref false in
+  let callback = 
+    function `YES -> rc := true | `NO -> rc := false | _ -> rc := false
   in
-  ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
-  connect_button dialog#confirmationDialogOkButton (return true);
-  connect_button dialog#confirmationDialogCancelButton (return false);
-  if not cancel then dialog#confirmationDialogCancelButton#misc#hide ();
-  dialog#confirmationDialog#show ();
-  GtkThread.main ();
-  (match !result with None -> assert false | Some r -> r)
-
+  let buttons = GWindow.Buttons.yes_no in
+  try
+    popup_message ~title ~message ~message_type:`WARNING ~callback ~buttons
+      ?parent ();
+    !rc
+  with
+  | PopupClosed -> false
+
+let report_error ~title ~message ?parent () =
+  let rc = ref false in
+  let callback _ = () in
+  let buttons = GWindow.Buttons.ok in
+  try 
+    popup_message ~title ~message ~message_type:`ERROR ~callback ~buttons 
+    ?parent ()
+  with
+  | PopupClosed -> ()
+  
 let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
   let dialog = gui#newEmptyDialog () in
   dialog#emptyDialog#set_title title;

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index d18ff281d7f29e7a82cb0188bc5b7da775c83c86..8a9f8d6fbbd763129fc0e823e063fb8ca2b338d6 100644 (file)
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -107,13 +107,18 @@ class type gui =
 
   (** {3 Dialogs} *)
 
-  (** @return true if user hit "ok" button, false if user hit "cancel" button
-  * @param cancel if set to true a cancel button is shown to the user, otherwise
-  *   it is not (and indeed the function will return true). Defaults to true *)
+  (* @param parent to center the window on it *)
 val ask_confirmation:
-  gui:#gui ->
-  ?cancel:bool -> ?title:string -> ?msg:string -> unit ->
-    bool
+  title:string -> 
+  message:string -> 
+  ?parent:#GWindow.window_skel ->
+    unit -> bool
+
+val report_error:
+  title:string -> 
+  message:string -> 
+  ?parent:#GWindow.window_skel ->
+    unit -> unit
 
   (** @param multiline (default: false) if true a TextView widget will be used
   * for prompting the user otherwise a TextEntry widget will be

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) () =

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 5b1f4d5b39e79426ba911dc0e7bc782603a5f167..7b25b375c24a367469942d618faca21edd58eedb 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -350,9 +350,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
-  let fail msg =
-    ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
-      ~title:"Cic browser" ~msg ~cancel:false ());
+  let fail message = 
+    MatitaGtkMisc.report_error ~title:"Cic browser" ~message ()  
   in
   let tags =
     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");