Closed herbelin closed 5 years ago
Thanks for this PR. I merged it since it seems to be innocuous.
I'm still wondering whether we really need the destroy_with_parent
parameter, or whether it should be implicitly set to true for this kind of utility function.
Also you're right that it would make sense to apply it to all the similar dialogs.
I'm still wondering whether we really need the destroy_with_parent parameter, or whether it should be implicitly set to true for this kind of utility function. Also you're right that it would make sense to apply it to all the similar dialogs.
I can do both if you want, while I'm on it.
It would indeed make the functions more coherent.
In CoqIDE, we use message and question boxes but, when switching between applications, they easily get lost behind the main window, while still blocking actions on the main window. Attaching such a box to a main window with gtk's
gtk_window_set_transient_for
would solve this problem.This PR adds an optional parameter to
GToolbox.message_box
andGToolbox.question_box
to indicate a parent to which to be attached. To be consistent, it also adds adestroy_with_parent
parameter, though it is unclear that this would is the best design choice. Maybe, for simplicity, passing a parent should forcedestroy_with_parent
to be set to true by default?It is also unclear whether
parent
should be added to the other tool boxes (tree_selection_dialog
,input_widget
). I can extend the PR to them if there is a request for it.