X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=8a7048bbdf4cd7557213d78a064c9d2ee34385a2;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=4af50ee12393281c3c14cc1b510715e3c4dd2718;hpb=ea737dcc8aa007d39ee1c80bb0a96cb364cc3e22;p=helm.git diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 4af50ee12..8a7048bbd 100644 --- 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) () =