From 0ec7ec7e380b64c57e60d50025edcfc926fc861f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 26 Dec 2018 21:46:50 +0100 Subject: [PATCH] Quit without saving dialog fixed Ported to gtk3 --- matita/matita/matitaGtkMisc.ml | 45 ++++++++++----------------------- matita/matita/matitaGtkMisc.mli | 3 +-- matita/matita/matitaGui.ml | 2 +- 3 files changed, 16 insertions(+), 34 deletions(-) diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml index 765ffb33e..53546a903 100644 --- a/matita/matita/matitaGtkMisc.ml +++ b/matita/matita/matitaGtkMisc.ml @@ -272,19 +272,17 @@ let popup_message m#destroy () let popup_message_lowlevel - ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons + ~title ~message ?(no_separator=true) ~message_type ~buttons ?parent ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width - ?height ?(show=true) () + ?height () = let m = GWindow.dialog - ~no_separator - ?parent ~destroy_with_parent - ~title ?icon ~modal ~resizable ?screen - ?type_hint ~position ?wmclass ?border_width ?width ?height - ~show:false () + ?parent ~destroy_with_parent + ~title ?icon ~resizable ?screen + ?type_hint ~position ?wmclass ?border_width ?width ?height () in let stock = match message_type with @@ -302,34 +300,19 @@ let popup_message_lowlevel 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 + m#add_button_stock x 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 res = m#run () in + m#destroy () ; + res let ask_confirmation ~title ~message ?parent () = - let rc = ref `YES in - let callback = - function - | `YES -> rc := `YES - | `NO -> rc := `NO - | `CANCEL -> rc := `CANCEL - | `DELETE_EVENT -> rc := `CANCEL - | `POPUPCLOSED -> rc := `CANCEL - in - let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`CANCEL] in - popup_message_lowlevel - ~title ~message ~message_type:`WARNING ~callback ~buttons ?parent (); - !rc + GtkThread.sync (fun _ -> + let buttons = [`YES,`YES ; `NO,`NO ; `CANCEL,`DELETE_EVENT] in + popup_message_lowlevel + ~title ~message ~message_type:`WARNING ~buttons ?parent () + ) () let report_error ~title ~message ?parent () = let callback _ = () in diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli index 627909cd4..04a531216 100644 --- a/matita/matita/matitaGtkMisc.mli +++ b/matita/matita/matitaGtkMisc.mli @@ -122,8 +122,7 @@ class type gui = val ask_confirmation: title:string -> message:string -> ?parent:#GWindow.window_skel -> - unit -> - [`YES | `NO | `CANCEL] + unit -> [`YES | `NO | `DELETE_EVENT ] val report_error: title:string -> message:string -> diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 4dc6274a3..ee268e60a 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -931,7 +931,7 @@ class gui () = save_moo script#status; true | `NO -> true - | `CANCEL -> false + | `DELETE_EVENT -> false else (save_moo script#status; true) -- 2.39.2