indexing
	description: "Set and get the double-click time for the mouse."
	status: "See notice at end of class."
	date: "$Date$"
	revision: "$Revision$"

class interface
	WEL_DOUBLE_CLICK

feature -- Status report

	double_click_time: INTEGER
			-- Current double-click time for the mouse (in milliseconds)
		ensure
			positive_result: Result > 0
	
feature -- Status setting

	set_double_click_time (time: INTEGER)
			-- Set double_click_time with time (in milliseconds).
		require
			positive_time: time > 0
		ensure
			double_click_time_set: double_click_time = time
	
invariant

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

end -- class WEL_DOUBLE_CLICK