diff options
| author | Hugo Herbelin | 2018-11-11 15:05:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-11 15:44:10 +0100 |
| commit | 008354e71473ecdae0ca34dd5af951c4a4ae18dc (patch) | |
| tree | c33905849291b5272ef9b2e9e76e3b8153c9a368 | |
| parent | 35a11a5567d660e545ad39c03b9bef39c26380ba (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.ml | 37 | ||||
| -rw-r--r-- | ide/configwin_ihm.mli | 9 |
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 |
