diff options
Diffstat (limited to 'otherlibs/labltk/browser/jg_message.mli')
| -rw-r--r-- | otherlibs/labltk/browser/jg_message.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/jg_message.mli b/otherlibs/labltk/browser/jg_message.mli new file mode 100644 index 000000000..8862702c6 --- /dev/null +++ b/otherlibs/labltk/browser/jg_message.mli @@ -0,0 +1,13 @@ +(* $Id$ *) + +val formatted : + title:string -> + ?on:Widget.frame Widget.widget -> + ?width:int -> + ?maxheight:int -> + ?minheight:int -> + unit -> Widget.any Widget.widget * Widget.text Widget.widget * (unit -> unit) + +val ask : + title:string -> ?master:Widget.toplevel Widget.widget -> + string -> [`cancel|`no|`yes] |