From b47af4383d51dae275964d464e6a8faf2a5a3f51 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Jun 2005 13:08:02 +0000
Subject: [PATCH] fixed some errers in the save/cancel ...

---
 helm/matita/matitaGtkMisc.ml | 14 ++++++++------
 helm/matita/matitaGui.ml     |  4 +++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index b8c9b91b3..b0624241a 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -218,11 +218,15 @@ let popup_message_lowlevel
   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));
   GtkThread.main ();
   m#destroy () 
 
@@ -235,14 +239,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
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fa6059d1e..b21c3b340 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -262,7 +262,9 @@ class gui () =
                 ()
             in
             match rc with
-            | `YES -> saveScript ();GMain.Main.quit ()
+            | `YES -> saveScript ();
+                      if not source_view#buffer#modified then
+                        GMain.Main.quit ()
             | `NO -> GMain.Main.quit ()
             | `CANCEL -> ()
           end else GMain.Main.quit ());
-- 
2.39.2