From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 26 Dec 2018 20:46:50 +0000 (+0100)
Subject: Quit without saving dialog fixed
X-Git-Tag: make_still_working~229^2~1^2~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ad99cc72c725c0cceda7ddf3dbaafedfe4dcb5b2

Quit without saving dialog fixed

Ported to gtk3
---

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)