From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 24 Dec 2018 00:05:41 +0000 (+0100)
Subject: disambiguationErrors now uses #run
X-Git-Tag: make_still_working~229^2~1^2~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adc35b2abd4f832f4a879e87f6fc3d0a05f78071;p=helm.git

disambiguationErrors now uses #run

correct Gtk behavior
---

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index e001f1db0..d7642d04e 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -318,11 +318,12 @@ let interactive_error_interp ~all_passes
           (MultiPassDisambiguator.DisambiguationError
             (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
+      GtkThread.sync (fun _ ->
        let dialog = new disambiguationErrors () in
-   dialog#toplevel#add_button "Fix this interpretation" `OK;
-   dialog#toplevel#add_button "Close" `DELETE_EVENT;
-   if not all_passes then
-    dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
+       dialog#toplevel#add_button "Fix this interpretation" `OK;
+       dialog#toplevel#add_button "Close" `DELETE_EVENT;
+       if not all_passes then
+        dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
        let model = new interpErrorModel dialog#treeview choices in
        dialog#disambiguationErrors#set_title "Disambiguation error";
        dialog#disambiguationErrorsLabel#set_label
@@ -354,8 +355,7 @@ let interactive_error_interp ~all_passes
             (MultiPassDisambiguator.DisambiguationError
               (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
-   dialog#toplevel#show ();
-   ignore(dialog#toplevel#connect#response (function
+   (match GtkThread.sync dialog#toplevel#run () with
     | `OK ->
        let tree_path =
         match fst (dialog#treeview#get_cursor ()) with
@@ -391,13 +391,14 @@ let interactive_error_interp ~all_passes
          source_buffer#insert
           ~iter:
             (source_buffer#get_iter_at_mark
-             (`NAME "beginning_of_statement")) newtxt ;
-         dialog#toplevel#destroy ()
+             (`NAME "beginning_of_statement")) newtxt
     | `HELP (* HELP MEANS MORE *) ->
-        dialog#toplevel#destroy ();
+        dialog#toplevel#destroy () ;
         raise UseLibrary
-    | `DELETE_EVENT -> dialog#toplevel#destroy ()
-    | _ -> assert false))
+    | `DELETE_EVENT -> ()
+    | _ -> assert false) ;
+   dialog#toplevel#destroy ()
+  ) ()
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)