From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 26 Dec 2018 21:01:16 +0000 (+0100)
Subject: report_error dialog ported to gtk3
X-Git-Tag: make_still_working~229^2~1^2~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5f4714c72188f1fc8fa0d9bb86f80b1b17ac6d7f

report_error dialog ported to gtk3
---

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 53546a903..52da5b420 100644
--- a/matita/matita/matitaGtkMisc.ml
+++ b/matita/matita/matitaGtkMisc.ml
@@ -25,7 +25,6 @@
 
 (* $Id$ *)
 
-exception PopupClosed
 open Printf
 
 let wrap_callback0 f = fun _ -> try f () with Not_found -> assert false
@@ -250,7 +249,7 @@ class type gui =
   end
 
 let popup_message 
-  ~title ~message ~buttons ~callback
+  ~title ~message ~buttons
   ?(message_type=`QUESTION) ?parent ?(use_markup=true)
   ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false)
   ?screen ?type_hint
@@ -264,11 +263,7 @@ let popup_message
       ?type_hint ~position ?wmclass ?border_width ?width ?height 
       ~show () 
   in 
-  ignore(m#connect#response 
-    ~callback:(fun a ->  GMain.Main.quit ();callback a));
-  ignore(m#connect#close 
-    ~callback:(fun _ -> GMain.Main.quit ();raise PopupClosed));
-  GtkThread.main ();
+  ignore(m#run ()) ;
   m#destroy () 
 
 let popup_message_lowlevel
@@ -315,14 +310,8 @@ let ask_confirmation ~title ~message ?parent () =
  ) ()
 
 let report_error ~title ~message ?parent () =
-  let callback _ = () in
-  let buttons = GWindow.Buttons.ok in
-  try 
-    popup_message 
-      ~title ~message ~message_type:`ERROR ~callback ~buttons ?parent ()
-  with
-  | PopupClosed -> ()
-
+ let buttons = GWindow.Buttons.ok in
+ popup_message ~title ~message ~message_type:`ERROR ~buttons ?parent ()
 
 let utf8_parsed_text s floc = 
   let start, stop = HExtlib.loc_of_floc floc in