From: Claudio Sacerdoti Coen 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;hp=6f24874d21e1ba9187599d0817c9ac8185a2464e;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 *)