X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGtkMisc.ml;h=1f3caa9c738c9fc7d415a9682bed3bd326ef3364;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=53546a90389f8eeee425c4dcc08f7e67f40d15d1;hpb=ad99cc72c725c0cceda7ddf3dbaafedfe4dcb5b2;p=helm.git

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 53546a903..1f3caa9c7 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
@@ -99,7 +98,7 @@ class multiStringListModel ~cols (tree_view: GTree.view) =
       (fun renderer -> GTree.view_column ~renderer ())
       renderers
   in
-  object (self)
+  object
     val text_columns = text_columns
     
     initializer
@@ -174,7 +173,7 @@ class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list)
   let lookup_pixbuf tag =
     try List.assoc tag tags with Not_found -> assert false
   in
-  object (self)
+  object
     initializer
       tree_view#set_model (Some (list_store :> GTree.model));
       ignore (tree_view#append_column tag_vcolumn);
@@ -228,7 +227,7 @@ class recordModel (tree_view:GTree.view) =
         ])
   in
   let toggle_vcol = GTree.view_column ~renderer:toggle_rend () in
-  object (self)
+  object
     initializer
       tree_view#set_model (Some (list_store :> GTree.model));
       ignore (tree_view#append_column text_vcol);
@@ -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,17 +263,13 @@ 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
-  ~title ~message ?(no_separator=true) ~message_type ~buttons
+  ~title ~message ?no_separator:(_=true) ~message_type ~buttons
   ?parent  ?(destroy_with_parent=true)
-  ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
+  ?icon ?modal:(_=true) ?(resizable=false) ?screen ?type_hint
   ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width 
   ?height ()
 =
@@ -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