Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

em.widget

Class EM_WIDGET_OPTIONS



Creation

Features

Invariants

indexing

description

Global options for all widgets.

Use EM_SHARED_WIDGET_OPTIONS to access the singleton instance.

date

$Date: 2005/10/23 11:17:50 $

revision

$Revision: 1.8 $

class

EM_WIDGET_OPTIONS

create {EM_SHARED_WIDGET_OPTIONS}

make

-- Initialise default values.

feature -- Access

tooltip_show_delay: INTEGER

-- Time to wait before tooltip is shown

feature -- Status report

are_tooltips_enabled: BOOLEAN

-- Are tooltips enabled?

is_dialog_dragging_restriction_enabled: BOOLEAN

-- Are dialogs restricted to coordinates inside scene?

is_transparency_refresh_enabled: BOOLEAN

-- Are transparent parts always refresh?
-- When transparency is used but a constant refresh of transparent areas is not
-- necessary, disable this option to improve performance.

feature -- Status setting

disable_dialog_dragging_restriction

-- Disable restriction of dialog dragging.

ensure
dialog_dragging_restriction_disabled: not is_dialog_dragging_restriction_enabled
disable_tooltips

-- Disable tooltips

ensure
tooltips_disabled: not are_tooltips_enabled
disable_transparency_refresh

-- Disable transparency refresh.

ensure
transparency_refresh_disabled: not is_transparency_refresh_enabled
enable_dialog_dragging_restriction

-- Enable restriction of dialog dragging.

ensure
dialog_dragging_restriction_enabled: is_dialog_dragging_restriction_enabled
enable_tooltips

-- Enable tooltips.

ensure
tooltips_enabled: are_tooltips_enabled
enable_transparency_refresh

-- Enable transparency refresh.

ensure
transparency_refresh_enabled: is_transparency_refresh_enabled

feature -- Element change

set_tooltip_show_delay (a_value: like tooltip_show_delay)

-- Set tooltip_show_delay to a_value.

ensure
tooltip_show_delay_set: tooltip_show_delay = a_value

invariant

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end