]> matita.cs.unibo.it Git - helm.git/commitdiff
the error_report window is now properly closed
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 29 Jun 2005 09:01:30 +0000 (09:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 29 Jun 2005 09:01:30 +0000 (09:01 +0000)
helm/matita/matitaGtkMisc.ml

index b53bbd209dad6ee860c48be855d699fe4036a835..4af50ee12393281c3c14cc1b510715e3c4dd2718 100644 (file)
@@ -186,7 +186,8 @@ let popup_message
     ~callback:(fun a ->  GMain.Main.quit ();callback a));
   ignore(m#connect#close 
     ~callback:(fun _ -> GMain.Main.quit ();raise PopupClosed));
-  GtkThread.main ()
+  GtkThread.main ();
+  m#destroy () 
 
 
 let ask_confirmation ~title ~message ?parent () =
@@ -206,12 +207,14 @@ let report_error ~title ~message ?parent () =
   let rc = ref false in
   let callback _ = () in
   let buttons = GWindow.Buttons.ok in
-  try 
+(  try 
     popup_message ~title ~message ~message_type:`ERROR ~callback ~buttons 
     ?parent ()
   with
   | PopupClosed -> ()
-  
+);prerr_endline "AAAAAAA" 
+
+
 let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
   let dialog = gui#newEmptyDialog () in
   dialog#emptyDialog#set_title title;