* http://helm.cs.unibo.it/
*)
+exception PopupClosed
open Printf
open MatitaTypes
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;