15.3.727  src/lib/x-kit/widget/old/wrapper/border.api

## border.api
#
# Border widget -- draws a border around its child.
#
#     "The ability to specify a border of an X window is a
#      programming convenience in simple applications, and
#      improves performance by allowing the server to
#      perform damage control on boders which would otherwise
#      have to be performed by the application.  On the
#      negative side, the use of borders unnecessarily
#      complicates the coputation of window geometries.
#      Knowing the upper left corner of a window and the
#      size of its drawing region is not enough to calculate
#      the actual bounding box of the window; the window's
#      border must be taken into account.
#
#     "For these reasons, the [x-kit] widget library assumes
#      all underlying X windows will have borders of width
#      zero. To provide borders, the library supplies
#      [border] widgets.  A [border] widgets creates a
#      border of a given size and color around its child
#      widget."
#
#           -- p15-16 of Gansner+Reppy's 1993 eXene widget manual
#              http://mythryl.org/pub/exene/1993-widgets.ps
#
# A border widget is effectively transparent
# except for its border.  It inherits its
# parent's background color.  The set_color()
# call may be used to change border color dynamically.
#
# The size preferences of a border widget are those
# of its child, increased by border width.

# Compiled by:
#     src/lib/x-kit/widget/xkit-widget.sublib


# Compiled by:
#     src/lib/x-kit/widget/xkit-widget.sublib

# This api is implemented in:
# 
#     src/lib/x-kit/widget/old/wrapper/border.pkg

stipulate
    package wg =  widget;                       # widget        is from   src/lib/x-kit/widget/old/basic/widget.pkg
    package xc =  xclient;                      # xclient       is from   src/lib/x-kit/xclient/xclient.pkg
herein

    api Border {

        Border;

        border:  (wg::Root_Window, wg::View, List(wg::Arg)) -> wg::Widget -> Border;

        make_border
            :
            { color:  Null_Or( xc::Rgb ),               # Border color, defaults to paren't background color.
              width:  Int,                              # Border width in pixels.
              child:  wg::Widget                        # Child widget.
            }
            ->
            Border;
                #
                # A negative border width raises exception BAD_ARG.

        as_widget:  Border -> wg::Widget;

        set_color:  Border -> Null_Or(xc::Rgb) -> Void;
            #
            # Dynamically change border color.
    };

end;