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

em.widget.input

Class EM_KEYBOARD_FOCUS



Features

Invariants

indexing

description

Store and manage the keyboard focus. Used by EM_WIDGET_SCENE and
EM_COMPONENT_SCENE to set and retreive the keyboard focus.

Use EM_SHARED_FOCUS to access the singleton instance.

date

$Date: 2005/10/23 11:21:01 $

revision

$Revision: 1.7 $

class

EM_KEYBOARD_FOCUS

feature -- Access

current_focus: EM_KEYBOARD_SENSITIVE

-- Current keyboard focus

default_focus: like current_focus

-- Default keyboard focus

feature -- Status report

has_focus: BOOLEAN

-- Is a focus present?

feature -- Element change

set_current_focus (an_object: like current_focus)

-- Set current_focus to an_object.

ensure
focus_set_to_an_object: an_object /= Void implies current_focus = an_object
focus_set_to_default: an_object = Void implies current_focus = default_focus
set_default_focus (an_object: like default_focus)

-- Set default_focus to an_object

ensure
default_focus_set: default_focus = an_object

feature {EM_COMPONENT_SCENE, EM_COMPONENT} -- Implementation

new_focus: like current_focus

-- The focus to be set when checking phase is over

set_new_focus (an_object: like new_focus)

-- Set new_focus to an_object.

ensure
new_focus_set: new_focus = an_object
start_check

-- Start checking for a new keyboard focus.

stop_check

-- Stop checking for a new keyboard focus.
-- Set the keyboard focus to new_focus.

invariant

consistent: has_focus implies current_focus /= Void
default_focus_if_no_other: current_focus = Void implies default_focus = Void

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

end