version 0.7.1

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 4af50ee12393281c3c14cc1b510715e3c4dd2718..8a7048bbdf4cd7557213d78a064c9d2ee34385a2 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -29,13 +29,6 @@ open Printf
 open MatitaTypes
 
 let wrap_callback f = f
-(*
-let wrap_callback f () =
-  try
-    f ()
-  with exn ->
-    MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
-*)
 
 let connect_button (button: #GButton.button) callback =
   ignore (button#connect#clicked (wrap_callback callback))
@@ -189,30 +182,75 @@ let popup_message
   GtkThread.main ();
   m#destroy () 
 
+let popup_message_lowlevel
+  ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons
+  ?parent  ?(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.dialog 
+      ~no_separator 
+      ?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:false () 
+  in
+  let stock = 
+    match message_type with
+    | `WARNING -> `DIALOG_WARNING
+    | `INFO -> `DIALOG_INFO
+    | `ERROR ->`DIALOG_ERROR 
+    | `QUESTION -> `DIALOG_QUESTION
+  in
+  let image = GMisc.image ~stock ~icon_size:`DIALOG () in
+  let label = GMisc.label ~markup:message () in
+  label#set_line_wrap true;
+  let hbox = GPack.hbox ~spacing:10 () in
+  hbox#pack ~from:`START ~expand:true ~fill:true (image:>GObj.widget);
+  hbox#pack ~from:`START ~expand:true ~fill:true (label:>GObj.widget);
+  m#vbox#pack ~from:`START 
+    ~padding:20 ~expand:true ~fill:true (hbox:>GObj.widget);
+  List.iter (fun (x, y) -> 
+    m#add_button_stock x y;
+    if y = `CANCEL then 
+      m#set_default_response y
+  ) buttons;
+  ignore(m#connect#response 
+    ~callback:(fun a ->  GMain.Main.quit ();callback a));
+  ignore(m#connect#close 
+    ~callback:(fun _ -> GMain.Main.quit ();callback `POPUPCLOSED));
+  if show = true then 
+      m#show ();
+  GtkThread.main ();
+  m#destroy () 
+
 
 let ask_confirmation ~title ~message ?parent () =
-  let rc = ref false in
+  let rc = ref `YES in
   let callback = 
-    function `YES -> rc := true | `NO -> rc := false | _ -> rc := false
+    function 
+    | `YES -> rc := `YES
+    | `NO -> rc := `NO
+    | `CANCEL -> rc := `CANCEL
+    | `DELETE_EVENT -> rc := `CANCEL
+    | `POPUPCLOSED -> rc := `CANCEL
   in
-  let buttons = GWindow.Buttons.yes_no in
-  try
-    popup_message ~title ~message ~message_type:`WARNING ~callback ~buttons
-      ?parent ();
+  let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`CANCEL] in
+    popup_message_lowlevel 
+      ~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 ()
+  try 
+    popup_message 
+      ~title ~message ~message_type:`ERROR ~callback ~buttons ?parent ()
   with
   | PopupClosed -> ()
-);prerr_endline "AAAAAAA" 
 
 
 let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =