X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGtkMisc.ml;h=52da5b420569864f8e8e01bcdc102400c8896a22;hb=5f4714c72188f1fc8fa0d9bb86f80b1b17ac6d7f;hp=53546a90389f8eeee425c4dcc08f7e67f40d15d1;hpb=ad99cc72c725c0cceda7ddf3dbaafedfe4dcb5b2;p=helm.git diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml index 53546a903..52da5b420 100644 --- a/matita/matita/matitaGtkMisc.ml +++ b/matita/matita/matitaGtkMisc.ml @@ -25,7 +25,6 @@ (* $Id$ *) -exception PopupClosed open Printf let wrap_callback0 f = fun _ -> try f () with Not_found -> assert false @@ -250,7 +249,7 @@ class type gui = end let popup_message - ~title ~message ~buttons ~callback + ~title ~message ~buttons ?(message_type=`QUESTION) ?parent ?(use_markup=true) ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint @@ -264,11 +263,7 @@ let popup_message ?type_hint ~position ?wmclass ?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 (); + ignore(m#run ()) ; m#destroy () let popup_message_lowlevel @@ -315,14 +310,8 @@ let ask_confirmation ~title ~message ?parent () = ) () let report_error ~title ~message ?parent () = - let callback _ = () in - let buttons = GWindow.Buttons.ok in - try - popup_message - ~title ~message ~message_type:`ERROR ~callback ~buttons ?parent () - with - | PopupClosed -> () - + let buttons = GWindow.Buttons.ok in + popup_message ~title ~message ~message_type:`ERROR ~buttons ?parent () let utf8_parsed_text s floc = let start, stop = HExtlib.loc_of_floc floc in