X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=8a7048bbdf4cd7557213d78a064c9d2ee34385a2;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=b8c9b91b3308b327ce14015248338a4ac0f9d17d;hpb=fccf05646ed2e47a81290a2884191edbddcaa169;p=helm.git diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index b8c9b91b3..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)) @@ -202,7 +195,7 @@ let popup_message_lowlevel ?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 () + ~show:false () in let stock = match message_type with @@ -213,16 +206,23 @@ let popup_message_lowlevel 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) buttons; + 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 ();raise PopupClosed)); + ~callback:(fun _ -> GMain.Main.quit ();callback `POPUPCLOSED)); + if show = true then + m#show (); GtkThread.main (); m#destroy () @@ -235,14 +235,12 @@ let ask_confirmation ~title ~message ?parent () = | `NO -> rc := `NO | `CANCEL -> rc := `CANCEL | `DELETE_EVENT -> rc := `CANCEL + | `POPUPCLOSED -> rc := `CANCEL in - let buttons = [`CANCEL,`CANCEL ; `NO,`NO ; `YES,`YES] in - try + let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`CANCEL] in popup_message_lowlevel ~title ~message ~message_type:`WARNING ~callback ~buttons ?parent (); !rc - with - | PopupClosed -> `CANCEL let report_error ~title ~message ?parent () = let rc = ref false in