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

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

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;