aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2018-11-11 15:05:58 +0100
committerHugo Herbelin2018-11-11 15:44:10 +0100
commit008354e71473ecdae0ca34dd5af951c4a4ae18dc (patch)
treec33905849291b5272ef9b2e9e76e3b8153c9a368
parent35a11a5567d660e545ad39c03b9bef39c26380ba (diff)
A private copy of lablgtk's question_box supporting the "parent" option.
The "parent" option allows to attach the box to the parent box. This ensures that the dialog box, which blocks action on the main window, does not get hidden by the main window. Idem for the message_box.
-rw-r--r--ide/configwin_ihm.ml37
-rw-r--r--ide/configwin_ihm.mli9
2 files changed, 46 insertions, 0 deletions
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index a6a3d52a38..91695e944e 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -808,3 +808,40 @@ let custom ?label box f expand =
custom_expand = expand ;
custom_framed = label ;
}
+
+(* Copying lablgtk question_box + forbidding hiding *)
+
+let question_box ~title ~buttons ?(default=1) ?icon ?parent message =
+ let button_nb = ref 0 in
+ let window = GWindow.dialog ~position:`CENTER ~modal:true ?parent ~type_hint:`DIALOG ~title () in
+ let hbox = GPack.hbox ~border_width:10 ~packing:window#vbox#add () in
+ let bbox = window#action_area in
+ begin match icon with
+ None -> ()
+ | Some i -> hbox#pack i#coerce ~padding:4
+ end;
+ ignore (GMisc.label ~text: message ~packing: hbox#add ());
+ (* the function called to create each button by iterating *)
+ let rec iter_buttons n = function
+ [] ->
+ ()
+ | button_label :: q ->
+ let b = GButton.button ~label: button_label
+ ~packing:(bbox#pack ~expand:true ~padding:4) ()
+ in
+ ignore (b#connect#clicked ~callback:
+ (fun () -> button_nb := n; window#destroy ()));
+ (* If it's the first button then give it the focus *)
+ if n = default then b#grab_default () else ();
+
+ iter_buttons (n+1) q
+ in
+ iter_buttons 1 buttons;
+ ignore (window#connect#destroy ~callback: GMain.Main.quit);
+ window#set_position `CENTER;
+ window#show ();
+ GMain.Main.main ();
+ !button_nb
+
+let message_box ~title ?icon ?parent ?(ok="Ok") message =
+ ignore (question_box ?icon ?parent ~title message ~buttons:[ ok ])
diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli
index 94a3f12b39..772a0958ff 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
@@ -65,3 +65,12 @@ val edit :
?height:int ->
configuration_structure list ->
return_button
+
+val question_box : title:string ->
+ buttons:string list ->
+ ?default:int -> ?icon:#GObj.widget ->
+ ?parent:GWindow.window -> string -> int
+
+val message_box :
+ title:string -> ?icon:#GObj.widget ->
+ ?parent:GWindow.window -> ?ok:string -> string -> unit