Quelle ui_dialogs.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type button_contents =
| ButtonWithStock of GtkStock.id
| ButtonWithLabel of string

let question_box ?parent ?icon ~title ?(buttons = []) ?(default = 1) 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:15 ~packing:window#vbox#add () in
  let bbox = window#action_area in
  Option.iter (fun icon -> hbox#pack icon#coerce ~padding:4) icon;
  ignore (GMisc.label ~text:message ~packing:hbox#add ());
  (* the function called to create each button by iterating *)
  let rec iter_buttons pos = function
  | but_content :: others ->
      let label, stock =
        match but_content with
        | ButtonWithLabel label -> Some label, None
        | ButtonWithStock stock -> None, Some stock
      in
      let but = GButton.button ?label ?stock ~packing:(bbox#pack ~expand:true) () in
      ignore (but#connect#clicked ~callback:(fun () -> button_nb := pos; window#destroy ()));
      (* If it's the default button then give it the focus *)
      if pos = default then
        but#grab_default ();
      iter_buttons (pos + 1) others;
  | [] -> ()
  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 ?parent ?icon ~title ?(ok = ButtonWithStock `OK) message =
  ignore (question_box ?parent ?icon ~title ~buttons:[ ok ] message)

quality96%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.