world-attributes

Vocabulary

ui.gadgets.worlds

Inputs

None

Outputs

None

Class description

Tuples of this class can be passed to open-window to control attributes of the window opened. The following attributes can be set:

•	world-class specifies the class of world to construct. world is the default.
•	title is the window title.
•	status, if specified, is a gadget that will be used as the window's status bar.
•	gadgets is a sequence of gadgets that will be placed inside the window.
•	pixel-format-attributes is a sequence of Pixel format attributes that the window will request for its OpenGL pixel format.
•	window-controls is a sequence of Window controls that will be placed in the window.

See also

worlds, open-window, find-window

Definition

USING: strings ui.pixel-formats ;

IN: ui.gadgets.worlds

TUPLE: world-attributes
    { world-class initial: world } grab-input?
    { title string initial: "Factor Window" } status gadgets {
        pixel-format-attributes initial:
        { windowed double-buffered }
    } {
        window-controls initial: {
            normal-title-bar
            close-button
            minimize-button
            maximize-button
            resize-handles
        }
    } pref-dim
    { fill initial: 1 } { orientation initial: { 0 1 } } ;