Automatic generation produced by ISE Eiffel
note description: "EiffelVision menu. Mswindows implementation." legal: "See notice at end of class." status: "See notice at end of class." date: "$Date: 2017-03-27 09:23:22 -0800 (Mon, 27 Mar 2017) $" revision: "$Revision: 100056 $" class interface EV_MENU_IMP create make -- Initialize Current. require -- from EV_ANY_I True ensure -- from EV_ANY_I is_initialized: get_state_flag (Is_initialized_flag) feature -- Initialization make -- Initialize Current. require -- from EV_ANY_I True ensure -- from EV_ANY_I is_initialized: get_state_flag (Is_initialized_flag) old_make (an_interface: attached like interface) -- Create underlying native toolkit objects. -- Every descendant should exactly one a creation procedure `make`. -- Must call base_make. require -- from EV_ANY_I an_interface_not_void: an_interface /= Void ensure -- from EV_ANY_I interface_assigned: interface = an_interface base_make_called: base_make_called feature -- Access accept_cursor: detachable EV_POINTER_STYLE -- Accept cursor set by user. -- To be displayed when the screen pointer is over a target that accepts -- `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE_I) awaiting_movement: BOOLEAN -- Are we currently awaiting the movement threshold to -- be reached for as drag and drop or dockable move? -- (from EV_SHARED_TRANSPORT_IMP) caption_font: WEL_FONT -- Caption font -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists capture_enabled: BOOLEAN -- Is the mouse currently captured? -- See constants Capture_xxxx at the end of the class. -- (from EV_PICK_AND_DROPABLE_IMP) check_drag_and_drop_release (a_x, a_y: INTEGER_32) -- End transport if in drag and drop. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) configurable_target_menu_handler: detachable PROCEDURE [EV_MENU, ARRAYED_LIST [EV_PND_TARGET_DATA], EV_PICK_AND_DROPABLE, detachable ANY] -- (from EV_PICK_AND_DROPABLE_I) cursor: EV_DYNAMIC_LIST_CURSOR [EV_MENU_ITEM] -- Current cursor position. -- (from EV_DYNAMIC_LIST_I) ensure -- from EV_DYNAMIC_LIST_I not_void: Result /= Void deny_cursor: detachable EV_POINTER_STYLE -- Deny cursor set by user. -- To be displayed when the screen pointer is not over a valid target. -- (from EV_PICK_AND_DROPABLE_I) Drag_and_drop_starting_movement: INTEGER_32 = 3 -- Pointer movement in pixels required to start a drag and drop. -- (from EV_SHARED_TRANSPORT_IMP) escape_pnd -- Escape the pick and drop. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) ensure -- from EV_PICK_AND_DROPABLE_IMP not_in_transport: not transport_executing generating_type: TYPE [detachable EV_MENU_IMP] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) ensure -- from ANY generating_type_not_void: Result /= Void generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty gui_font: WEL_FONT -- Default screen (WEL) font. -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists Gwl_exstyle: INTEGER_32 = -20 -- (from WEL_GWL_CONSTANTS) Gwl_style: INTEGER_32 = -16 -- (from WEL_GWL_CONSTANTS) has_heavy_capture: BOOLEAN -- Does `parent` have a heavy capture? -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) i_th (i: INTEGER_32): like item -- Item at i-th position. -- (from EV_DYNAMIC_LIST_IMP) require -- from EV_DYNAMIC_LIST_I i_within_bounds: i > 0 and then i <= count ensure -- from EV_DYNAMIC_LIST_I not_void: Result /= Void id: INTEGER_32 -- Unique identifier within system. -- (from EV_ID_IMP) index: INTEGER_32 -- Index of current position -- (from EV_DYNAMIC_LIST_I) index_of (v: detachable like item; i: INTEGER_32): INTEGER_32 -- Index of i_th item v, if present. -- As dynamic list descendants are all sets, -- Result will be zero for all values of i -- that are not equal to one -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I positive_occurrences: i > 0 item: EV_MENU_ITEM -- Current item -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I readable: index > 0 and then index <= count ensure -- from EV_DYNAMIC_LIST_I not_void: Result /= Void wel_item: POINTER -- Generic Windows handle or structure pointer. -- Can be a HWND, HICON, RECT *, WNDCLASS *, etc... -- (from WEL_ANY) item_by_data (data: ANY): detachable like item -- First item with data. -- (from EV_ITEM_LIST_I) require -- from EV_ITEM_LIST_I data_not_void: data /= Void Mb_abortretryignore: INTEGER_32 = 2 -- (from WEL_MB_CONSTANTS) Mb_applmodal: INTEGER_32 = 0 -- (from WEL_MB_CONSTANTS) Mb_default_desktop_only: INTEGER_32 = 131072 -- (from WEL_MB_CONSTANTS) Mb_defbutton1: INTEGER_32 = 0 -- (from WEL_MB_CONSTANTS) Mb_defbutton2: INTEGER_32 = 256 -- (from WEL_MB_CONSTANTS) Mb_defbutton3: INTEGER_32 = 512 -- (from WEL_MB_CONSTANTS) Mb_defmask: INTEGER_32 = 3840 -- (from WEL_MB_CONSTANTS) Mb_help: INTEGER_32 = 16384 -- (from WEL_MB_CONSTANTS) Mb_iconasterisk: INTEGER_32 = 64 -- (from WEL_MB_CONSTANTS) Mb_iconerror: INTEGER_32 = 16 -- Same as `mb_iconhand`. -- (from WEL_MB_CONSTANTS) Mb_iconexclamation: INTEGER_32 = 48 -- (from WEL_MB_CONSTANTS) Mb_iconhand: INTEGER_32 = 16 -- (from WEL_MB_CONSTANTS) Mb_iconinformation: INTEGER_32 = 64 -- Same as `mb_iconasterisk`. -- (from WEL_MB_CONSTANTS) Mb_iconmask: INTEGER_32 = 240 -- (from WEL_MB_CONSTANTS) Mb_iconquestion: INTEGER_32 = 32 -- (from WEL_MB_CONSTANTS) Mb_iconstop: INTEGER_32 = 16 -- Same as `mb_iconhand`. -- (from WEL_MB_CONSTANTS) Mb_iconwarning: INTEGER_32 = 48 -- Same as `mb_iconexclamation`. -- (from WEL_MB_CONSTANTS) Mb_nofocus: INTEGER_32 = 32768 -- (from WEL_MB_CONSTANTS) Mb_ok: INTEGER_32 = 0 -- (from WEL_MB_CONSTANTS) Mb_okcancel: INTEGER_32 = 1 -- (from WEL_MB_CONSTANTS) Mb_retrycancel: INTEGER_32 = 5 -- (from WEL_MB_CONSTANTS) Mb_right: INTEGER_32 = 524288 -- (from WEL_MB_CONSTANTS) Mb_rtlreading: INTEGER_32 = 1048576 -- (from WEL_MB_CONSTANTS) Mb_setforeground: INTEGER_32 = 65536 -- (from WEL_MB_CONSTANTS) Mb_systemmodal: INTEGER_32 = 4096 -- (from WEL_MB_CONSTANTS) Mb_taskmodal: INTEGER_32 = 8192 -- (from WEL_MB_CONSTANTS) Mb_topmost: INTEGER_32 = 262144 -- (from WEL_MB_CONSTANTS) Mb_typemask: INTEGER_32 = 15 -- (from WEL_MB_CONSTANTS) Mb_usericon: INTEGER_32 = 128 -- (from WEL_MB_CONSTANTS) Mb_yesno: INTEGER_32 = 4 -- (from WEL_MB_CONSTANTS) Mb_yesnocancel: INTEGER_32 = 3 -- (from WEL_MB_CONSTANTS) menu_font: WEL_FONT -- Font used in menus -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists message_font: WEL_FONT -- Font used in message boxes -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists Mf_append: INTEGER_32 = 256 -- (from WEL_MF_CONSTANTS) Mf_bitmap: INTEGER_32 = 4 -- (from WEL_MF_CONSTANTS) Mf_bycommand: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_byposition: INTEGER_32 = 1024 -- (from WEL_MF_CONSTANTS) Mf_change: INTEGER_32 = 128 -- (from WEL_MF_CONSTANTS) Mf_checked: INTEGER_32 = 8 -- (from WEL_MF_CONSTANTS) Mf_delete: INTEGER_32 = 512 -- (from WEL_MF_CONSTANTS) Mf_disabled: INTEGER_32 = 2 -- (from WEL_MF_CONSTANTS) Mf_enabled: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_end: INTEGER_32 = 128 -- (from WEL_MF_CONSTANTS) Mf_grayed: INTEGER_32 = 1 -- (from WEL_MF_CONSTANTS) Mf_help: INTEGER_32 = 16384 -- (from WEL_MF_CONSTANTS) Mf_hilite: INTEGER_32 = 128 -- (from WEL_MF_CONSTANTS) Mf_insert: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_menubarbreak: INTEGER_32 = 32 -- (from WEL_MF_CONSTANTS) Mf_menubreak: INTEGER_32 = 64 -- (from WEL_MF_CONSTANTS) Mf_mouseselect: INTEGER_32 = 32768 -- (from WEL_MF_CONSTANTS) Mf_ownerdraw: INTEGER_32 = 256 -- (from WEL_MF_CONSTANTS) Mf_popup: INTEGER_32 = 16 -- (from WEL_MF_CONSTANTS) Mf_remove: INTEGER_32 = 4096 -- (from WEL_MF_CONSTANTS) Mf_separator: INTEGER_32 = 2048 -- (from WEL_MF_CONSTANTS) Mf_string: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_sysmenu: INTEGER_32 = 8192 -- (from WEL_MF_CONSTANTS) Mf_unchecked: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_unhilite: INTEGER_32 = 0 -- (from WEL_MF_CONSTANTS) Mf_usecheckbitmaps: INTEGER_32 = 512 -- (from WEL_MF_CONSTANTS) object_id: INTEGER_32 -- Run-time object Id of Current. -- (from EV_MENU_ITEM_IMP) off: BOOLEAN -- Is there no current item? -- (from EV_DYNAMIC_LIST_I) original_pressure: REAL_64 -- Hold the values passed to start transport so when a transport -- actually starts, with real_start_transport,these can be passed -- as arguments. -- (from EV_SHARED_TRANSPORT_IMP) original_x: INTEGER_32 -- (from EV_SHARED_TRANSPORT_IMP) original_x_tilt: REAL_64 -- Hold the values passed to start transport so when a transport -- actually starts, with real_start_transport,these can be passed -- as arguments. -- (from EV_SHARED_TRANSPORT_IMP) original_y: INTEGER_32 -- (from EV_SHARED_TRANSPORT_IMP) original_y_tilt: REAL_64 -- Hold the values passed to start transport so when a transport -- actually starts, with real_start_transport,these can be passed -- as arguments. -- (from EV_SHARED_TRANSPORT_IMP) pebble: detachable ANY -- Data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) pebble_function: detachable FUNCTION [detachable ANY] -- Returns data to be transported by pick and drop mechanism. -- (from EV_PICK_AND_DROPABLE_I) pebble_positioning_enabled: BOOLEAN -- If True then pick and drop start coordinates are -- `pebble_x_position`, `pebble_y_position`. -- If False then pick and drop start coordinates are -- the pointer coordinates. -- (from EV_PICK_AND_DROPABLE_I) pebble_x_position: INTEGER_32 -- Initial x position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) pebble_y_position: INTEGER_32 -- Initial y position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) pixmap: detachable EV_PIXMAP -- Give a copy of pixmap used by Current. -- (from EV_PIXMAPABLE_IMP) require -- from EV_PIXMAPABLE_I True pixmap_imp: detachable EV_PIXMAP_IMP_STATE -- Implementation of pixmap in Current. -- (from EV_PIXMAPABLE_IMP) pnd_original_parent: detachable EV_PICK_AND_DROPABLE_ITEM_HOLDER_IMP -- Actual widget parent of Current when PND starts. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) pnd_press (a_x, a_y, a_button, a_screen_x, a_screen_y: INTEGER_32) -- Process a pointer press that may alter the current state -- of pick/drag and drop. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) popup_menu (position: INTEGER_32): WEL_MENU -- Popup menu at the zero-based relative position -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count popup_exists: popup_exists (position) ensure -- from WEL_MENU result_not_void: Result /= Void retrieve_item_by_data (data: detachable ANY; should_compare_objects: BOOLEAN): detachable EV_MENU_ITEM -- Result is first item in Current with data -- matching some_data. Compare objects if -- should_compare_objects otherwise compare references. -- (from EV_DYNAMIC_LIST_I) retrieve_items_by_data (data: ANY; should_compare_objects: BOOLEAN): ARRAYED_LIST [EV_MENU_ITEM] -- Result is all items in Current with data -- matching some_data. Compare objects if -- should_compare_objects otherwise compare references. -- (from EV_DYNAMIC_LIST_I) set_pnd_original_parent -- Assign `parent_imp` to `pnd_original_parent`. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) set_pointer_style (c: EV_POINTER_STYLE) -- Assign c to `parent_imp` pointer style. -- (from EV_PICK_AND_DROPABLE_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_I True small_caption_font: WEL_FONT -- Small caption font -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists status_font: WEL_FONT -- Font used in status bars -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS result_exists: Result /= Void and then Result.exists system_color_3dface: WEL_COLOR_REF -- Face color for three-dimensional display elements and -- for dialog box backgrounds. -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnface`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_3dhighlight: WEL_COLOR_REF -- Highlight color for three-dimensional display elements -- (for edges facing the light source.) -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnhighlight`, `system_color_btnhilight` and `system_color_3dhilight`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_3dhilight: WEL_COLOR_REF -- Highlight color for three-dimensional display elements -- (for edges facing the light source.) -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnhighlight`, `system_color_btnhilight` and `system_color_3dhighlight`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_3dshadow: WEL_COLOR_REF -- Shadow color for three-dimensional display elements -- (for edges facing away from the light source). -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnshadow`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_activeborder: WEL_COLOR_REF -- Color for active window border. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_activecaption: WEL_COLOR_REF -- Color for active window title bar. -- -- Windows 98, Windows 2000: Specifies the left side color in the -- color gradient of an active window's title bar if the gradient -- effect is enabled. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_appworkspace: WEL_COLOR_REF -- Background color of multiple document interface -- (MDI) applications. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_background: WEL_COLOR_REF -- Color of the desktop -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_desktop`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_btnface: WEL_COLOR_REF -- Face color for three-dimensional display elements and -- for dialog box backgrounds. -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_3dface`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_btnhighlight: WEL_COLOR_REF -- Highlight color for three-dimensional display elements -- (for edges facing the light source.) -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnhilight`, `system_color_3dhighlight` and `system_color_3dhilight`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_btnhilight: WEL_COLOR_REF -- Highlight color for three-dimensional display elements -- (for edges facing the light source.) -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_btnhighlight`, `system_color_3dhighlight` and `system_color_3dhilight`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_btnshadow: WEL_COLOR_REF -- Shadow color for three-dimensional display elements -- (for edges facing away from the light source). -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_3dshadow`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_btntext: WEL_COLOR_REF -- Color of text on push buttons. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_captiontext: WEL_COLOR_REF -- Color for text in caption, size box, and -- scroll bar arrow box. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_desktop: WEL_COLOR_REF -- Color of the desktop -- Was declared in {WEL_SYSTEM_COLORS} as synonym of `system_color_background`. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_gradientactivecaption: WEL_COLOR_REF -- Right side color in the color gradient of an active window's -- title bar. `system_color_activecaption` specifies the left side color. -- (from WEL_SYSTEM_COLORS) require -- from WEL_SYSTEM_COLORS windows_98_required: (create {WEL_WINDOWS_VERSION} end).is_windows_98_compatible ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_gradientinactivecaption: WEL_COLOR_REF -- Right side color in the color gradient of an inactive window's -- title bar. `system_color_inactivecaption` specifies the left side color. -- (from WEL_SYSTEM_COLORS) require -- from WEL_SYSTEM_COLORS windows_98_required: (create {WEL_WINDOWS_VERSION} end).is_windows_98_compatible ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_graytext: WEL_COLOR_REF -- Color for grayed (disabled) text. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_highlight: WEL_COLOR_REF -- Color for item(s) selected in a control. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_highlighttext: WEL_COLOR_REF -- Color for text of item(s) selected in a control. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_hotlight: WEL_COLOR_REF -- Color for a hot-tracked item. Single clicking a hot-tracked item executes the item. -- (Windows 98/Me, Windows 2000 or later) -- (from WEL_SYSTEM_COLORS) require -- from WEL_SYSTEM_COLORS windows_98_required: (create {WEL_WINDOWS_VERSION} end).is_windows_98_compatible ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_inactiveborder: WEL_COLOR_REF -- Color for inactive window border. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_inactivecaption: WEL_COLOR_REF -- Color for inactive window caption. -- -- Windows 98, Windows 2000: Specifies the left side color in the -- color gradient of an inactive window's title bar if the gradient -- effect is enabled. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_inactivecaptiontext: WEL_COLOR_REF -- Color of text in an inactive caption. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_info_text: WEL_COLOR_REF -- Background color for tooltip text -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_infobk: WEL_COLOR_REF -- Background color for tooltip -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_menu: WEL_COLOR_REF -- background color for menus. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_menubar: WEL_COLOR_REF -- The background color for the menu bar when menus appear as flat menus (see SystemParametersInfo). -- However, `system_color_menu` continues to specify the background color of the menu popup. -- (from WEL_SYSTEM_COLORS) require -- from WEL_SYSTEM_COLORS windows_xp_required: (create {WEL_WINDOWS_VERSION} end).is_windows_xp_compatible ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_menuhilight: WEL_COLOR_REF -- The color used to highlight menu items when the menu appears as a flat menu (see SystemParametersInfo). -- The highlighted menu item is outlined with `system_color_highlight`. -- (from WEL_SYSTEM_COLORS) require -- from WEL_SYSTEM_COLORS windows_xp_required: (create {WEL_WINDOWS_VERSION} end).is_windows_xp_compatible ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_menutext: WEL_COLOR_REF -- Color for text in menus. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_scrollbar: WEL_COLOR_REF -- Color for the scroll bar gray area. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_window: WEL_COLOR_REF -- background for windows. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_windowframe: WEL_COLOR_REF -- Color for window frame. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_color_windowtext: WEL_COLOR_REF -- Color for text in windows. -- (from WEL_SYSTEM_COLORS) ensure -- from WEL_SYSTEM_COLORS result_exists: Result /= Void system_font: WEL_FONT -- Default system font. -- (from WEL_SHARED_FONTS) ensure -- from WEL_SHARED_FONTS font_created: Result /= Void and then Result.exists text: STRING_32 -- Text displayed in label. -- (from EV_MENU_ITEM_IMP) require -- from EV_TEXTABLE_I True ensure -- from EV_TEXTABLE_I not_void: Result /= Void cloned: Result /= text tpm_bottomalign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_centeralign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_leftalign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_leftbutton: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_returncmd: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_rightalign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_rightbutton: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_topalign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) tpm_vcenteralign: INTEGER_32 -- (from WEL_TPM_CONSTANTS) transport_executing: BOOLEAN -- Is a pick and drop or drag and drop currently -- being executed? -- (from EV_PICK_AND_DROPABLE_IMP) Wel_color_constants: WEL_COLOR_CONSTANTS -- Access to COLOR_xxx constants. -- (from WEL_CONSTANTS) Wel_drawing_constants: WEL_DRAWING_CONSTANTS -- Drawing Constants -- Include constants: -- DI_xxxx -- DT_xxxx -- ... -- (from WEL_CONSTANTS) Wel_ht_constants: WEL_HT_CONSTANTS -- Access to Ht_xxxconstnats -- (from WEL_CONSTANTS) Wel_input_constants: WEL_INPUT_CONSTANTS -- Mouse Constants -- Include constants: -- MA_xxxx -- ... -- (from WEL_CONSTANTS) Wel_list_view_constants: WEL_LIST_VIEW_CONSTANTS -- ListView Control Constants -- Include constants: -- LVM_xxxx -- LVS_xxxx -- LVN_xxxx -- ... -- (from WEL_CONSTANTS) Wel_ownerdraw_constants: WEL_ODS_CONSTANTS -- Owner Drawing Constants -- Include constants: -- ODS_xxxx -- ... -- (from WEL_CONSTANTS) Wel_window_constants: WEL_WINDOW_CONSTANTS -- Window managment constants: -- Include constants: -- WM_xxxx -- ... -- (from WEL_CONSTANTS) widget_imp_at_pointer_position: detachable EV_WIDGET_IMP -- Result is implementation of widget at current -- pointer position or Void if none. -- (from EV_SHARED_TRANSPORT_IMP) feature -- Measurement count: INTEGER_32 -- Number of items. -- (from EV_DYNAMIC_LIST_IMP) require -- from EV_DYNAMIC_LIST_I True wel_count: INTEGER_32 -- Number of items -- (from WEL_MENU) require -- from WEL_MENU exists: exists ensure -- from WEL_MENU positive_result: Result >= 0 dpi: NATURAL_32 -- Window dpi. -- (from EV_POSITIONED_I) height: INTEGER_32 -- Vertical size in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True minimum_height: INTEGER_32 -- Minimum vertical size in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True minimum_width: INTEGER_32 -- Minimum horizontal size in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True screen_x: INTEGER_32 -- Horizontal offset relative to screen. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True require -- from EV_ITEM_LIST_IMP True screen_y: INTEGER_32 -- Vertical offset relative to screen. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True require -- from EV_ITEM_LIST_IMP True width: INTEGER_32 -- Horizontal size in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True x_position: INTEGER_32 -- Horizontal offset relative to parent `x_position` in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True y_position: INTEGER_32 -- Vertical offset relative to parent `y_position` in pixels. -- (from EV_MENU_ITEM_IMP) require -- from EV_POSITIONED_I True feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) frozen is_deep_equal alias "≡≡≡" (other: EV_MENU_IMP): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) is_equal (other: EV_MENU_IMP): BOOLEAN -- Is other attached to an object considered -- equal to current object? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) frozen standard_is_equal alias "≜" (other: EV_MENU_IMP): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) feature -- Status report conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void exists: BOOLEAN -- Does the `item` exist? -- (from WEL_ANY) ensure -- from WEL_ANY Result = (wel_item /= default_pointer) flag_set (flags, mask: INTEGER_32): BOOLEAN -- Is mask set in flags? -- (from WEL_BIT_OPERATIONS) foreground_window: detachable WEL_WINDOW -- Foreground window (window with focus) -- (from WEL_WINDOWS_ROUTINES) has (v: detachable like item): BOOLEAN -- Does structure contain v? -- (from EV_DYNAMIC_LIST_I) id_string (an_id: INTEGER_32): STRING_32 -- String associated with an_id -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU result_not_void: Result /= Void internal_non_sensitive: BOOLEAN -- Is Current not sensitive to input as seen -- from `interface`? -- (from EV_SENSITIVE_I) is_destroyed: BOOLEAN -- Is Current no longer usable? -- (from EV_ANY_I) is_sensitive: BOOLEAN -- Can this item be clicked on? -- user from setting the sensitive state while unparented. -- (from EV_MENU_ITEM_IMP) is_terminal_service: BOOLEAN -- If window in terminal service (Remote Desktop)? -- (from WEL_WINDOWS_ROUTINES) require -- from WEL_WINDOWS_ROUTINES after_2000: (create {WEL_WINDOWS_VERSION} end).is_windows_2000_compatible is_transport_enabled: BOOLEAN -- Is the transport mechanism enabled? -- (from EV_PICK_AND_DROPABLE_I) is_window (hwnd: POINTER): BOOLEAN -- Does hwnd point to a valid Window? -- (from WEL_WINDOWS_ROUTINES) item_checked (an_id: INTEGER_32): BOOLEAN -- Is the item idenfied by an_id checked? -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) item_enabled (an_id: INTEGER_32): BOOLEAN -- Is the item idenfied by an_id enabled? -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) item_exists (an_id: INTEGER_32): BOOLEAN -- Does an_id exist in the menu? -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 key_down (virtual_key: INTEGER_32): BOOLEAN --Is 'virtual' key pressed -- (from WEL_WINDOWS_ROUTINES) key_locked (virtual_key: INTEGER_32): BOOLEAN --Is 'virtual' key locked -- (from WEL_WINDOWS_ROUTINES) key_to_string (key_data: INTEGER_32): STRING_32 -- Give the string associated with the key given by -- virtual_key. -- (from WEL_WINDOWS_ROUTINES) mode_is_configurable_target_menu: BOOLEAN -- Is the transport mechanism a configurable target menu? -- (from EV_PICK_AND_DROPABLE_I) mode_is_drag_and_drop: BOOLEAN -- Is the transport mechanism drag and drop? -- (from EV_PICK_AND_DROPABLE_I) mode_is_pick_and_drop: BOOLEAN -- Is the transport mechanism pick and drop? -- (from EV_PICK_AND_DROPABLE_I) mode_is_target_menu: BOOLEAN -- Is the transport mechanism a target menu? -- (from EV_PICK_AND_DROPABLE_I) popup_exists (position: INTEGER_32): BOOLEAN -- Does a popup menu exists at the zero-based position? -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_position: position >= 0 position_enabled (position: INTEGER_32): BOOLEAN -- Is the item at zero-based position enabled? -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) shared: BOOLEAN -- Is `item` shared by another object? -- If False (by default), `item` will -- be destroyed by `destroy_item`. -- If True, `item` will not be destroyed. -- (from WEL_ANY) system_directory: STRING_32 -- Path of the Windows system directory -- (from WEL_WINDOWS_ROUTINES) ensure -- from WEL_WINDOWS_ROUTINES result_not_void: Result /= Void tick_count: INTEGER_32 -- Number of milliseconds that have -- elapsed since Windows was started. -- (from WEL_WINDOWS_ROUTINES) ensure -- from WEL_WINDOWS_ROUTINES positive_result: Result >= 0 user_is_sensitive: BOOLEAN -- Is the object sensitive to user input. -- (from EV_SENSITIVE_I) valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? -- This is True if p conforms to EV_DYNAMIC_LIST_CURSOR and -- if it points to an item, Current must have it. -- (from EV_DYNAMIC_LIST_I) window_of_item (hwnd: POINTER): detachable WEL_WINDOW -- Retrieve Eiffel object associated with hwnd pointer. -- (from WEL_WINDOWS_ROUTINES) require -- from WEL_WINDOWS_ROUTINES hwnd_not_null: hwnd /= default_pointer is_window_pointer: is_window (hwnd) ensure -- from WEL_WINDOWS_ROUTINES is_wel_window: Result /= Void end implies (create {INTERNAL} end).type_conforms_to ((create {INTERNAL} end).dynamic_type (Result), (create {INTERNAL} end).dynamic_type_from_string ("WEL_WINDOW")) is_proper_wel_window: Result /= Void implies Result.item = hwnd windows_directory: STRING_32 -- Path of the Windows directory -- (from WEL_WINDOWS_ROUTINES) ensure -- from WEL_WINDOWS_ROUTINES result_not_void: Result /= Void feature -- Status setting check_item (an_id: INTEGER_32) -- Put a check mark for the item identified by an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU item_checked: item_checked (an_id) disable_item (an_id: INTEGER_32) -- Disable the item identified by an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU item_disabled: not item_enabled (an_id) disable_pebble_positioning -- Assign False to `pebble_positioning_enabled`. -- (from EV_PICK_AND_DROPABLE_I) disable_position (position: INTEGER_32) -- Disable the item at zero-based position. -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count ensure -- from WEL_MENU position_disabled: not position_enabled (position) disable_transport -- Deactivate pick/drag and drop mechanism. -- (from EV_PICK_AND_DROPABLE_IMP) require -- from EV_PICK_AND_DROPABLE_I True ensure -- from EV_PICK_AND_DROPABLE_I is_transport_disabled: not is_transport_enabled enable_item (an_id: INTEGER_32) -- Enable the item idenfied by an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU item_enabled: item_enabled (an_id) enable_pebble_positioning -- Assign True to `pebble_positioning_enabled`. -- (from EV_PICK_AND_DROPABLE_I) enable_position (position: INTEGER_32) -- Enable the item at zero-based position. -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count ensure -- from WEL_MENU position_enabled: position_enabled (position) enable_transport -- Activate pick/drag and drop mechanism. -- (from EV_PICK_AND_DROPABLE_IMP) require -- from EV_PICK_AND_DROPABLE_I pebble_not_void: pebble /= Void or pebble_function /= Void ensure -- from EV_PICK_AND_DROPABLE_I is_transport_enabled: is_transport_enabled pnd_motion (a_x, a_y, a_screen_x, a_screen_y: INTEGER_32) -- If in drag/pick and drop then update. -- (from EV_PICK_AND_DROPABLE_IMP) remove_pebble -- Remove `pebble`. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pebble_removed: pebble = Void and pebble_function = Void is_transport_disabled: not is_transport_enabled reset_pebble_function -- Reset any values created by calling `pebble_function`. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pebble_function_preserved: pebble_function = old pebble_function pebble_without_function: pebble_function = Void implies (pebble = old pebble) pebble_with_function: pebble_function /= Void implies pebble = Void set_accept_cursor (a_cursor: like accept_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that accepts `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE_I) set_configurable_target_menu_handler (a_handler: like configurable_target_menu_handler) -- Set Configurable Target Menu Handler to a_handler. -- (from EV_PICK_AND_DROPABLE_I) set_configurable_target_menu_mode -- Set transport mechanism to a configurable target_menu. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I mode_is_target_menu: mode_is_configurable_target_menu set_deny_cursor (a_cursor: like deny_cursor) -- Set a_cursor to be displayed when the screen pointer is over a -- target that doesn't accept `pebble` during pick and drop. -- (from EV_PICK_AND_DROPABLE_I) set_drag_and_drop_mode -- Set transport mechanism to drag and drop, -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I mode_is_drag_and_drop: mode_is_drag_and_drop set_pebble (a_pebble: ANY) -- Assign a_pebble to `pebble`. -- (from EV_PICK_AND_DROPABLE_I) require -- from EV_PICK_AND_DROPABLE_I a_pebble_not_void: a_pebble /= Void ensure -- from EV_PICK_AND_DROPABLE_I pebble_assigned: pebble = a_pebble is_transport_enabled: is_transport_enabled set_pebble_function (a_function: FUNCTION [detachable ANY]) -- Assign a_function to `pebble_function`. -- (from EV_PICK_AND_DROPABLE_I) require -- from EV_PICK_AND_DROPABLE_I a_function_not_void: a_function /= Void ensure -- from EV_PICK_AND_DROPABLE_I pebble_function_assigned: pebble_function = a_function is_transport_enabled: is_transport_enabled set_pebble_position (a_x, a_y: INTEGER_32) -- Set the initial position for pick and drop relative to Current. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I pick_x_assigned: pick_x.to_integer_32 = a_x pick_y_assigned: pick_y.to_integer_32 = a_y set_pick_and_drop_mode -- Set transport mechanism to pick and drop, -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I mode_is_pick_and_drop: mode_is_pick_and_drop set_shared -- Set `shared` to True. -- (from WEL_ANY) ensure -- from WEL_ANY shared: shared set_target_menu_mode -- Set transport mechanism to a target_menu. -- (from EV_PICK_AND_DROPABLE_I) ensure -- from EV_PICK_AND_DROPABLE_I mode_is_target_menu: mode_is_target_menu set_unshared -- Set `shared` to False. -- (from WEL_ANY) ensure -- from WEL_ANY unshared: not shared show_configurable_target_menu (a_x, a_y: INTEGER_32) -- Show the configurable target menu at position a_x, a_y relative to Current. -- (from EV_PICK_AND_DROPABLE_I) uncheck_item (an_id: INTEGER_32) -- Remove the check mark for the item identified -- by an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU item_unchecked: not item_checked (an_id) user_disable_sensitive -- Make object desensitive to user input. -- (from EV_SENSITIVE_I) ensure -- from EV_SENSITIVE_I is_desensitive: not user_is_sensitive user_enable_sensitive -- Make object sensitive to user input. -- (from EV_SENSITIVE_I) ensure -- from EV_SENSITIVE_I is_sensitive_if_parent_sensitive: (has_parent and then parent_is_sensitive) implies attached_interface.implementation.is_sensitive is_sensitive_if_orphaned: not has_parent implies attached_interface.implementation.is_sensitive feature -- Cursor movement back -- Move to previous item. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I not_before: index > 0 forth -- Move cursor to next position. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I not_after: index <= count go_i_th (i: INTEGER_32) -- Move cursor to i-th position. -- (from EV_DYNAMIC_LIST_I) go_to (p: CURSOR) -- Move cursor to position p. -- (from EV_DYNAMIC_LIST_I) move (i: INTEGER_32) -- Move cursor i positions. -- (from EV_DYNAMIC_LIST_I) start -- Move cursor to first position. -- (from EV_DYNAMIC_LIST_I) ensure -- from EV_DYNAMIC_LIST_I index_on_first: index = 1 feature -- Element change append (s: SEQUENCE [EV_MENU_ITEM]) -- Append a copy of s. Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I sequence_not_void: s /= Void ensure -- from EV_DYNAMIC_LIST_I count_increased: old count + s.count = count append_bitmap (bitmap: WEL_BITMAP; an_id: INTEGER_32) -- Append bitmap with the identifier an_id to the -- menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists bitmap_not_void: bitmap /= Void bitmap_exists: bitmap.exists positive_id: an_id > 0 item_not_exists: not item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 item_exists: item_exists (an_id) append_popup (a_menu: WEL_MENU; a_title: READABLE_STRING_GENERAL) -- Append a popup menu a_menu with a_title to the -- current menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_menu_not_void: a_menu /= Void a_menu_exists: a_menu.exists a_title_not_void: a_title /= Void ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 append_separator -- Append a separator to the current menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 append_string (a_string: READABLE_STRING_GENERAL; an_id: INTEGER_32) -- Append a_string with the identifier an_id to the -- menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_string_not_void: a_string /= Void positive_id: an_id > 0 item_not_exists: not item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 item_exists: item_exists (an_id) string_set: id_string (an_id).same_string_general (a_string) append_string_with_break (a_string: READABLE_STRING_GENERAL; an_id: INTEGER_32; has_separator: BOOLEAN) -- Append an item with a break to the menu. -- All the following items will be set in a new column. -- If has_separator is True, then a vertical separator -- appears between the two columns. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_string_not_void: a_string /= Void positive_id: an_id > 0 item_not_exists: not item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 item_exists: item_exists (an_id) string_set: id_string (an_id).same_string_general (a_string) extend (v: like item) -- Add v to end. Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) insert_bitmap (bitmap: WEL_BITMAP; a_position, an_id: INTEGER_32) -- Insert bitmap at zero-based a_position with -- an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_position_large_enough: a_position >= 0 a_position_small_enough: a_position <= wel_count bitmap_not_void: bitmap /= Void bitmap_exists: bitmap.exists positive_id: an_id > 0 item_not_exists: not item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 insert_popup (a_menu: WEL_MENU; a_position: INTEGER_32; a_title: READABLE_STRING_GENERAL) -- Insert a popup menu a_menu at zero-based a_position -- with a_title. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_menu_not_void: a_menu /= Void a_menu_exists: a_menu.exists a_title_not_void: a_title /= Void a_position_large_enough: a_position >= 0 a_position_small_enough: a_position <= wel_count ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 popup_menu_set: popup_menu (a_position).item = a_menu.item insert_separator (a_position: INTEGER_32) -- Insert a separator at zero-based a_position. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_position_large_enough: a_position >= 0 a_position_small_enough: a_position <= wel_count ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 insert_string (a_string: READABLE_STRING_GENERAL; a_position, an_id: INTEGER_32) -- Insert a_string at zero-based a_position with -- an_id. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_position_large_enough: a_position >= 0 a_position_small_enough: a_position <= wel_count a_string_not_void: a_string /= Void positive_id: an_id > 0 item_not_exists: not item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count + 1 string_set: id_string (an_id).same_string_general (a_string) merge_left (other: like attached_interface) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other. -- (from EV_DYNAMIC_LIST_I) merge_right (other: like attached_interface) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. -- (from EV_DYNAMIC_LIST_I) modify_string (a_string: READABLE_STRING_GENERAL; an_id: INTEGER_32) -- Modify the menu title identified by an_id to -- a_string. -- (from WEL_MENU) require -- from WEL_MENU exists: exists a_string_not_void: a_string /= Void positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU string_set: id_string (an_id).same_string_general (a_string) pixmap_equal_to (a_pixmap: EV_PIXMAP): BOOLEAN -- Is a_pixmap equal to `pixmap`? -- (from EV_PIXMAPABLE_I) put_front (v: like item) -- Add v at beginning. Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) put_i_th (v: like item; i: INTEGER_32) -- Replace item at i-th position by v. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I valid_index: i > 0 and i <= count v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) put_left (v: like item) -- Add v to the left of cursor position. Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) put_right (v: like item) -- Add v to the right of cursor position. Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) replace (v: like item) -- Replace current item by v. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I writable: index > 0 and then index <= count v_not_void: v /= Void ensure -- from EV_DYNAMIC_LIST_I has_v: has (v) set_item (an_item: POINTER) -- Set `item` with an_item -- (from WEL_ANY) ensure -- from WEL_ANY item_set: wel_item = an_item set_parent_imp (a_parent_imp: like parent_imp) -- Make a_parent_imp the parent of Current. -- (from EV_MENU_ITEM_IMP) ensure -- from EV_ITEM_IMP assigned: parent_imp = a_parent_imp set_text (a_text: READABLE_STRING_GENERAL) -- Assign a_text to `text`. -- (from EV_MENU_ITEM_IMP) require -- from EV_TEXTABLE_I a_text_not_void: a_text /= Void no_carriage_returns: not a_text.has_code (('%R').natural_32_code) ensure -- from EV_TEXTABLE_I text_cloned: attached a_text as l_text and then text.same_string_general (l_text) and then text /= l_text feature -- Removal delete_item (an_id: INTEGER_32) -- Delete an_id from the menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists positive_id: an_id > 0 item_exists: item_exists (an_id) ensure -- from WEL_MENU new_count: wel_count = old wel_count - 1 item_not_exists: not item_exists (an_id) delete_position (position: INTEGER_32) -- Delete the item at zero-based position. -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count ensure -- from WEL_MENU new_count: wel_count = old wel_count - 1 prune (v: like item) -- Remove v if present. Do not move cursor, except if -- cursor was on v, move to right neighbor. -- (from EV_DYNAMIC_LIST_I) ensure -- from EV_DYNAMIC_LIST_I cursor_not_moved: not old has (v) implies old attached_interface.index = attached_interface.index cursor_not_moved: old has (v) and then old attached_interface.index < old index_of (v, 1) implies index = old index cursor_not_moved: old has (v) and then old attached_interface.index >= old index_of (v, 1) implies index = old index - 1 not_has_v: not has (v) remove -- Remove current item. Move cursor to right neighbor -- (or after if no right neighbor). -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I writable: not off ensure -- from EV_DYNAMIC_LIST_I not_has_v: not has (old item) remove_left -- Remove item to the left of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I left_exists: index > 1 not_before: not (index = 0) ensure then -- from EV_DYNAMIC_LIST_I left_neighbor_removed: not has (old i_th (index - 1)) remove_position (position: INTEGER_32) -- Remove the item at zero-based position. -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count ensure -- from WEL_MENU new_count: wel_count = old wel_count - 1 remove_right -- Remove item to the right of cursor position. -- Do not move cursor. -- (from EV_DYNAMIC_LIST_I) require -- from EV_DYNAMIC_LIST_I right_exists: index < count ensure then -- from EV_DYNAMIC_LIST_I right_neighbor_removed: not has (old i_th (index + 1)) wipe_out -- Remove all items. -- (from EV_DYNAMIC_LIST_I) feature -- Conversion position_to_item_id (position: INTEGER_32): INTEGER_32 -- Retrieve the menu item identifier of a menu item at -- the zero-based position. -- Return 0 if the item at the zero-based -- position is a separator or a pop-up menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists position_large_enough: position >= 0 position_small_enough: position < wel_count feature -- Duplication copy (other: EV_MENU_IMP) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other frozen deep_copy (other: EV_MENU_IMP) -- Effect equivalent to that of: -- `copy` (other . `deep_twin`) -- (from ANY) require -- from ANY other_not_void: other /= Void ensure -- from ANY deep_equal: deep_equal (Current, other) frozen deep_twin: EV_MENU_IMP -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) frozen standard_copy (other: EV_MENU_IMP) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_standard_equal: standard_is_equal (other) frozen standard_twin: EV_MENU_IMP -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) frozen twin: EV_MENU_IMP -- New object equal to Current -- `twin` calls `copy`; to change copying/twinning semantics, redefine `copy`. -- (from ANY) ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current feature -- Basic operations clear_flag (flags, mask: INTEGER_32): INTEGER_32 -- Clear the mask in flags -- (from WEL_BIT_OPERATIONS) ensure -- from WEL_BIT_OPERATIONS flag_unset: not flag_set (Result, mask) cwin_hi_word (value: POINTER): INTEGER_32 -- SDK HIWORD -- (from WEL_WORD_OPERATIONS) cwin_lo_word (value: POINTER): INTEGER_32 -- SDK LOWORD -- (from WEL_WORD_OPERATIONS) cwin_make_long (low, high: INTEGER_32): POINTER -- SDK MAKELONG -- (from WEL_WORD_OPERATIONS) cwin_make_lparam (low, high: INTEGER_32): POINTER -- SKD MAKELPARAM -- (from WEL_WORD_OPERATIONS) frozen default: detachable EV_MENU_IMP -- Default value of object's type -- (from ANY) frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.`default` for -- some p of type POINTER.) -- (from ANY) ensure -- from ANY instance_free: class default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) disable_sensitive -- Set Current insensitive. require -- from EV_SENSITIVE_I True frozen do_nothing -- Execute a null action. -- (from ANY) ensure -- from ANY instance_free: class eif_current_object_id: INTEGER_32 -- New identifier for Current -- (from IDENTIFIED_ROUTINES) ensure -- from IDENTIFIED_ROUTINES eif_current_object_id: Result > 0 inserted: eif_is_object_id_of_current (Result) eif_id_any_object (an_id: INTEGER_32): detachable ANY -- Object associated with an_id -- (from IDENTIFIED_ROUTINES) require -- from IDENTIFIED_ROUTINES an_id_non_negative: an_id >= 0 ensure -- from IDENTIFIED_ROUTINES instance_free: class eif_is_object_id_of_current (an_id: INTEGER_32): BOOLEAN -- Is an_id the associated object ID of Current. -- (from IDENTIFIED_ROUTINES) require -- from IDENTIFIED_ROUTINES an_id_non_negative: an_id >= 0 eif_object_id (an_object: ANY): INTEGER_32 -- New identifier for an_object -- (from IDENTIFIED_ROUTINES) ensure -- from IDENTIFIED_ROUTINES instance_free: class eif_object_id_positive: Result > 0 inserted: eif_id_any_object (Result) = an_object eif_object_id_free (an_id: INTEGER_32) -- Free the entry an_id -- (from IDENTIFIED_ROUTINES) require -- from IDENTIFIED_ROUTINES an_id_non_negative: an_id >= 0 ensure -- from IDENTIFIED_ROUTINES instance_free: class removed: eif_id_any_object (an_id) = Void enable_sensitive -- Set Current insensitive. require -- from EV_SENSITIVE_I True hide_cursor -- Hide the cursor. -- (from WEL_WINDOWS_ROUTINES) hilite_menu_item (window: WEL_COMPOSITE_WINDOW; an_id: INTEGER_32) -- Hilite the item identified by an_id in the -- window's menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists window_not_void: window /= Void window_exists: window.exists positive_id: an_id > 0 item_exists: item_exists (an_id) message_beep_asterisk -- Play the system asterisk waveform sound. -- (from WEL_WINDOWS_ROUTINES) message_beep_exclamation -- Play the system exclamation waveform sound. -- (from WEL_WINDOWS_ROUTINES) message_beep_hand -- Play the system hand waveform sound. -- (from WEL_WINDOWS_ROUTINES) message_beep_ok -- Play the system ok waveform sound. -- (from WEL_WINDOWS_ROUTINES) message_beep_question -- Play the system question waveform sound. -- (from WEL_WINDOWS_ROUTINES) output_debug_string (s: READABLE_STRING_GENERAL) -- Send a string s to the system debugger. -- (from WEL_WINDOWS_ROUTINES) require -- from WEL_WINDOWS_ROUTINES s_not_void: s /= Void redraw (window: WEL_COMPOSITE_WINDOW) -- Redraws the menu bar of the specified window. -- If the menu bar changes after the system has created the window, -- this function must be called to draw the changed menu bar. -- (from WEL_MENU) resource_string_id (an_id: INTEGER_32): STRING_32 -- String identified by an_id in the resource file. -- (from WEL_WINDOWS_ROUTINES) ensure -- from WEL_WINDOWS_ROUTINES result_not_void: Result /= Void set_cursor_position_absolute (x, y: INTEGER_32) -- Set the cursor position to x, y. -- (from WEL_WINDOWS_ROUTINES) set_flag (flags, mask: INTEGER_32): INTEGER_32 -- Set the mask in flags -- (from WEL_BIT_OPERATIONS) ensure -- from WEL_BIT_OPERATIONS flag_set: flag_set (Result, mask) show -- Pop up on the current pointer position. show_at (a_widget: detachable EV_WIDGET; a_x, a_y: INTEGER_32) -- Pop up on a_x, a_y relative to the top-left corner -- of a_widget. show_cursor -- Show the cursor. -- (from WEL_WINDOWS_ROUTINES) show_track (x, y: INTEGER_32; window: WEL_COMPOSITE_WINDOW) -- Show a track popup menu at the x and y absolute -- position. window will receive the selection in -- on_menu_command. -- (from WEL_MENU) require -- from WEL_MENU exists: exists not_empty: wel_count > 0 window_not_void: window /= Void window_exists: window.exists show_track_with_option (x, y: INTEGER_32; window: WEL_COMPOSITE_WINDOW; option: INTEGER_32; rect: detachable WEL_RECT) -- Show a track popup menu with option at -- the x and y absolute position. -- window will receive the selection in -- on_menu_command. -- rect specifies the portion of the screen -- in which the user can select without -- dismissing the popup menu. If this parameter -- is Void the popup menu is dismissed if the -- user clicks outside the popup menu -- (from WEL_MENU) require -- from WEL_MENU exists: exists not_empty: wel_count > 0 window_not_void: window /= Void window_exists: window.exists unhilite_menu_item (window: WEL_COMPOSITE_WINDOW; an_id: INTEGER_32) -- unhilite the item identified by an_id in the -- window's menu. -- (from WEL_MENU) require -- from WEL_MENU exists: exists window_not_void: window /= Void window_exists: window.exists positive_id: an_id > 0 item_exists: item_exists (an_id) feature -- Implementation destroy -- Destroy underlying native toolkit objects. -- Render Current unusable. -- Any feature calls after a call to destroy are -- invalid. require -- from EV_ANY_I True ensure -- from EV_ANY_I is_in_destroy_set: is_in_destroy is_destroyed_set: is_destroyed dispose -- Destroy the inner structure of Current. -- -- This function should be called by the GC when the -- object is collected or by the user if Current is -- no more usefull. require -- from DISPOSABLE True parent: detachable EV_MENU_ITEM_LIST -- Item list containing Current. -- (from EV_MENU_ITEM_IMP) require -- from EV_ITEM_I True parent_imp: detachable EV_MENU_ITEM_LIST_IMP -- The menu or menu-bar this item is in. -- (from EV_MENU_ITEM_IMP) remove_pixmap -- Remove pixmap from Current. -- (from EV_MENU_ITEM_IMP) require -- from EV_PIXMAPABLE_I True ensure -- from EV_PIXMAPABLE_I pixmap_removed: pixmap = Void set_pixmap (a_pixmap: EV_PIXMAP) -- Assign a_pixmap to `pixmap`. -- (from EV_MENU_ITEM_IMP) require -- from EV_PIXMAPABLE_I pixmap_not_void: a_pixmap /= Void top_level_window_imp: detachable EV_WINDOW_IMP -- Window containing Current in parenting hierarchy. -- (from EV_MENU_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_IMP True feature -- "Shell and Common controls" Versions Comctl32_version: INTEGER_32 -- Version of Comctl32.dll -- (from WEL_WINDOWS_VERSION) Shell32_version: INTEGER_32 -- Version of Shell32.dll -- (from WEL_WINDOWS_VERSION) Shlwapi_version: INTEGER_32 -- Version of Shlwapi.dll -- (from WEL_WINDOWS_VERSION) feature -- Access EV_DRAGABLE_SOURCE. dockable_dialog_target: detachable EV_DOCKABLE_DIALOG -- A dockable dialog that will be created as -- necessary. This is not a local, to avoid it -- being garbage collected. -- (from EV_SHARED_TRANSPORT_I) Global_drag_targets: ARRAYED_LIST [INTEGER_32] -- Shortcut to EV_APPLICATION.pnd_targets. -- (from EV_SHARED_TRANSPORT_I) frozen Insert_label: EV_CELL -- Label used to indicate where Current will be placed in target. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I result_not_void: Result /= Void Insert_label_imp: EV_CELL_I -- Once access to implementation of `insert_label`. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I Result /= Void Insert_sep: EV_TOOL_BAR_SEPARATOR -- Once access to a separator used to indicate the insertion position -- when moving tool bar items. -- (from EV_SHARED_TRANSPORT_I) Insert_sep_imp: EV_TOOL_BAR_SEPARATOR_I -- Once access to implementation of `insert_sep`. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I Result /= Void Internal_screen: EV_SCREEN -- Once access to an EV_SCREEN. -- (from EV_SHARED_TRANSPORT_I) original_x_offset: INTEGER_16 -- Original x_offset and original_y_offset of transport -- realtive to widget. Only used for dragable transports. -- (from EV_SHARED_TRANSPORT_I) original_y_offset: INTEGER_16 -- Original x_offset and original_y_offset of transport -- realtive to widget. Only used for dragable transports. -- (from EV_SHARED_TRANSPORT_I) originating_source: detachable EV_DOCKABLE_SOURCE_I -- Dragable source that originated the transport of source_being_dragged. -- (from EV_SHARED_TRANSPORT_I) remove_insert_label -- Remove `insert_label` from its current `parent`. -- We must handle a special case for cells. If the parent is a cell, -- then we remove the cell from its parent, and then restore it. -- Otherwise, when the label, removed, the cell keeps it size, and cells -- are normally used with real_target when the cell must -- not be visible. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I not_parented: Insert_label.parent = Void remove_insert_sep -- Ensure inset_sep is not parented. -- (from EV_SHARED_TRANSPORT_I) ensure -- from EV_SHARED_TRANSPORT_I not_parented: Insert_sep.parent = Void source_being_docked: detachable EV_DOCKABLE_SOURCE_I -- Dragable source currently being transported. May be a -- WIDGET_IMP or an EV_TOOL_BAR_BUTTON_IMP. -- (from EV_SHARED_TRANSPORT_I) feature -- Access EV_PICK_AND_DROPABLE. Default_accept_cursor: EV_POINTER_STYLE -- Used in lieu of a user defined `accept_cursor`. -- (from EV_SHARED_TRANSPORT_I) Default_deny_cursor: EV_POINTER_STYLE -- Used in lieu of a user defined `deny_cursor`. -- (from EV_SHARED_TRANSPORT_I) Default_pixmaps: EV_STOCK_PIXMAPS -- Default pixmaps -- (from EV_SHARED_TRANSPORT_I) Global_pnd_targets: HASH_TABLE [INTEGER_32, INTEGER_32] -- Shortcut to EV_APPLICATION.pnd_targets. -- (from EV_SHARED_TRANSPORT_I) rubber_band_is_drawn: BOOLEAN -- Is a rubber band line currently on the screen? -- (from EV_SHARED_TRANSPORT_I) feature -- Access common. pointer_x: INTEGER_16 -- (from EV_SHARED_TRANSPORT_I) pointer_y: INTEGER_16 -- (from EV_SHARED_TRANSPORT_I) feature -- Compatible Windows Versions is_windows_2000_compatible: BOOLEAN -- Is the current program running under Windows 2000 or above? -- (from WEL_WINDOWS_VERSION) is_windows_98_compatible: BOOLEAN -- Is the current program running under Windows 98 or above? -- (from WEL_WINDOWS_VERSION) is_windows_9x: BOOLEAN -- Is the current program running under Windows 9x -- (Windows 95, Windows 98, Windows Me, ...)? -- (from WEL_WINDOWS_VERSION) is_windows_me_compatible: BOOLEAN -- Is the current program running under Windows Me or above? -- (from WEL_WINDOWS_VERSION) is_windows_nt: BOOLEAN -- Is the current program running under a version of -- windows belonging to the NT family? -- (Windows NT 3.51, Windows NT4, Windows 2000, -- Windows XP Home/Professional, Windows Vista) -- (from WEL_WINDOWS_VERSION) is_windows_nt4_compatible: BOOLEAN -- Is the current program running under Windows NT4 or above? -- (from WEL_WINDOWS_VERSION) is_windows_xp_compatible: BOOLEAN -- Is the current program running under Windows XP or above? -- (from WEL_WINDOWS_VERSION) feature -- Conversion from Eiffel to Windows frozen to_lparam (i: INTEGER_32): POINTER -- Convert integer value i in a valid LPARAM value. -- (from WEL_DATA_TYPE) ensure -- from WEL_DATA_TYPE is_class: class frozen to_lresult (i: INTEGER_32): POINTER -- Convert integer value i in a valid LRESULT value. -- (from WEL_DATA_TYPE) ensure -- from WEL_DATA_TYPE is_class: class frozen to_wparam (i: INTEGER_32): POINTER -- Convert integer value i in a valid WPARAM value. -- (from WEL_DATA_TYPE) ensure -- from WEL_DATA_TYPE is_class: class feature -- Current Windows Version build_number: INTEGER_32 -- Build number of current operating system -- (from WEL_WINDOWS_VERSION) require -- from WEL_WINDOWS_VERSION windows_nt_family: is_windows_nt major_version: INTEGER_32 -- Major version of current operating system -- (from WEL_WINDOWS_VERSION) minor_version: INTEGER_32 -- Minor version of current operating system -- (from WEL_WINDOWS_VERSION) version_info: detachable WEL_OS_VERSION_INFO -- Associated WEL_OS_VERSION_INFO structure -- (from WEL_WINDOWS_VERSION) feature -- Event handling conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when a pebble that fits here is picked. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void drop_actions: EV_PND_ACTION_SEQUENCE -- Actions to be performed when a pebble is dropped here. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void item_select_actions: EV_MENU_ITEM_SELECT_ACTION_SEQUENCE -- Actions to be performed when a menu item is selected. -- (from EV_MENU_ITEM_LIST_ACTION_SEQUENCES_I) ensure -- from EV_MENU_ITEM_LIST_ACTION_SEQUENCES_I not_void: Result /= Void new_item_actions: EV_LITE_ACTION_SEQUENCE [EV_ITEM] -- Actions to be performed after an item is added. -- (from EV_ITEM_LIST_IMP) pick_actions: EV_PND_START_ACTION_SEQUENCE -- Actions to be performed when `pebble` is picked up. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void pick_ended_actions: EV_PND_FINISHED_ACTION_SEQUENCE -- Actions to be performed when a transport from Current ends. -- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I) ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES_I not_void: Result /= Void pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer button is pressed. -- (from EV_ITEM_ACTION_SEQUENCES_I) ensure -- from EV_ITEM_ACTION_SEQUENCES_I not_void: Result /= Void pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE -- Actions to be performed when screen pointer is double clicked. -- (from EV_ITEM_ACTION_SEQUENCES_I) ensure -- from EV_ITEM_ACTION_SEQUENCES_I not_void: Result /= Void pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE -- Actions to be performed when screen pointer moves. -- (from EV_ITEM_ACTION_SEQUENCES_I) ensure -- from EV_ITEM_ACTION_SEQUENCES_I not_void: Result /= Void remove_item_actions: EV_LITE_ACTION_SEQUENCE [EV_ITEM] -- Actions to be performed before an item is removed. -- (from EV_ITEM_LIST_IMP) select_actions: EV_NOTIFY_ACTION_SEQUENCE -- Actions to be performed when selected. -- (from EV_MENU_ITEM_ACTION_SEQUENCES_I) ensure -- from EV_MENU_ITEM_ACTION_SEQUENCES_I not_void: Result /= Void feature -- Exact Windows Versions is_windows_2000: BOOLEAN -- Is the current program running under Windows 2000? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows2000_is_nt: Result implies is_windows_nt is_windows_95: BOOLEAN -- Is the current program running under Windows 95 -- (OSR1, OSR2 or OSR2.5)? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows95_is_9x: Result implies is_windows_9x is_windows_98: BOOLEAN -- Is the current program running under Windows 98 -- (1st or 2nd edition)? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows98_is_9x: Result implies is_windows_9x is_windows_me: BOOLEAN -- Is the current program running under Windows Millenium Edition? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows_me_is_9x: Result implies is_windows_9x is_windows_nt4: BOOLEAN -- Is the current program running under Windows NT4? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows_nt4_is_nt: Result implies is_windows_nt is_windows_vista: BOOLEAN -- If the current program running under Windows Vista? -- (from WEL_WINDOWS_VERSION) is_windows_xp: BOOLEAN -- Is the current program running under Windows XP (Home or Professional)? -- (from WEL_WINDOWS_VERSION) ensure -- from WEL_WINDOWS_VERSION windows_xp_is_nt: Result implies is_windows_nt feature -- For dialogs frozen dwlp_dlgproc: INTEGER_32 -- (from WEL_GWL_CONSTANTS) frozen dwlp_msgresult: INTEGER_32 -- (from WEL_GWL_CONSTANTS) frozen dwlp_user: INTEGER_32 -- (from WEL_GWL_CONSTANTS) feature -- For windows Gwl_hinstance: INTEGER_32 = -6 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwlp_hinstance`. -- (from WEL_GWL_CONSTANTS) Gwl_hwndparent: INTEGER_32 = -8 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwlp_hwndparent`. -- (from WEL_GWL_CONSTANTS) Gwl_id: INTEGER_32 = -12 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwlp_id`. -- (from WEL_GWL_CONSTANTS) Gwl_userdata: INTEGER_32 = -21 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwlp_userdata`. -- (from WEL_GWL_CONSTANTS) Gwl_wndproc: INTEGER_32 = -4 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwlp_wndproc`. -- (from WEL_GWL_CONSTANTS) Gwlp_hinstance: INTEGER_32 = -6 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwl_hinstance`. -- (from WEL_GWL_CONSTANTS) Gwlp_hwndparent: INTEGER_32 = -8 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwl_hwndparent`. -- (from WEL_GWL_CONSTANTS) Gwlp_id: INTEGER_32 = -12 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwl_id`. -- (from WEL_GWL_CONSTANTS) Gwlp_userdata: INTEGER_32 = -21 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwl_userdata`. -- (from WEL_GWL_CONSTANTS) Gwlp_wndproc: INTEGER_32 = -4 -- Was declared in {WEL_GWL_CONSTANTS} as synonym of `gwl_wndproc`. -- (from WEL_GWL_CONSTANTS) feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY out_not_void: Result /= Void print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) ensure -- from ANY tagged_out_not_void: Result /= Void feature -- Pick and Drop release_capture -- Release user input. -- Works only on current windows thread. -- (from EV_MENU_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_IMP True release_heavy_capture -- Release user input -- Works on all windows threads. -- (from EV_MENU_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_IMP True set_capture -- Grab user input. -- Works only on current windows thread. -- (from EV_MENU_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_IMP True set_heavy_capture -- Grab user input. -- Works on all windows threads. -- (from EV_MENU_ITEM_IMP) require -- from EV_PICK_AND_DROPABLE_IMP True feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void feature -- Status get_non_client_metrics: WEL_NON_CLIENT_METRICS -- Retrieves the metrics associated with the nonclient area of -- nonminimized windows. -- If non-successful, default value -- (from WEL_SYSTEM_PARAMETERS_INFO) get_wheel_scroll_lines: INTEGER_32 -- Retrieves the number of lines that will be scrolled when the mouse wheel is rotated. -- (from WEL_SYSTEM_PARAMETERS_INFO) has_drag_full_windows: BOOLEAN -- Determines whether dragging of full windows is enabled. -- The pvParam parameter must point to a BOOL variable that -- receives TRUE if enabled, or FALSE otherwise. -- -- Windows 95: This flag is supported only if Windows Plus! -- is installed. See SPI_GETWINDOWSEXTENSION. -- (from WEL_SYSTEM_PARAMETERS_INFO) has_flat_menu: BOOLEAN -- Determines whether native User menus have flat menu appearance -- (from WEL_SYSTEM_PARAMETERS_INFO) has_windows95_plus: BOOLEAN -- Windows 95 only: Indicates whether the Windows extension, -- Windows Plus!, is installed. Set the uiParam parameter to 1. -- The pvParam parameter is not used. The function returns TRUE -- if the extension is installed, or FALSE if it is not. -- (from WEL_SYSTEM_PARAMETERS_INFO) feature -- SystemParameter (All Windows) Spi_getaccesstimeout: INTEGER_32 = 60 -- Declared in Windows as SPI_GETACCESSTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getanimation: INTEGER_32 = 72 -- Declared in Windows as SPI_GETANIMATION -- (from WEL_SPI_CONSTANTS) Spi_getbeep: INTEGER_32 = 1 -- Declared in Windows as SPI_GETBEEP -- (from WEL_SPI_CONSTANTS) Spi_getborder: INTEGER_32 = 5 -- Declared in Windows as SPI_GETBORDER -- (from WEL_SPI_CONSTANTS) Spi_getdefaultinputlang: INTEGER_32 = 89 -- Declared in Windows as SPI_GETDEFAULTINPUTLANG -- (from WEL_SPI_CONSTANTS) Spi_getdragfullwindows: INTEGER_32 = 38 -- Declared in Windows as SPI_GETDRAGFULLWINDOWS -- (from WEL_SPI_CONSTANTS) Spi_getfasttaskswitch: INTEGER_32 = 35 -- Declared in Windows as SPI_GETFASTTASKSWITCH -- (from WEL_SPI_CONSTANTS) Spi_getfilterkeys: INTEGER_32 = 50 -- Declared in Windows as SPI_GETFILTERKEYS -- (from WEL_SPI_CONSTANTS) Spi_getfontsmoothing: INTEGER_32 = 74 -- Declared in Windows as SPI_GETFONTSMOOTHING -- (from WEL_SPI_CONSTANTS) Spi_getgridgranularity: INTEGER_32 = 18 -- Declared in Windows as SPI_GETGRIDGRANULARITY -- (from WEL_SPI_CONSTANTS) Spi_gethighcontrast: INTEGER_32 = 66 -- Declared in Windows as SPI_GETHIGHCONTRAST -- (from WEL_SPI_CONSTANTS) Spi_geticonmetrics: INTEGER_32 = 45 -- Declared in Windows as SPI_GETICONMETRICS -- (from WEL_SPI_CONSTANTS) Spi_geticontitlelogfont: INTEGER_32 = 31 -- Declared in Windows as SPI_GETICONTITLELOGFONT -- (from WEL_SPI_CONSTANTS) Spi_geticontitlewrap: INTEGER_32 = 25 -- Declared in Windows as SPI_GETICONTITLEWRAP -- (from WEL_SPI_CONSTANTS) Spi_getkeyboarddelay: INTEGER_32 = 22 -- Declared in Windows as SPI_GETKEYBOARDDELAY -- (from WEL_SPI_CONSTANTS) Spi_getkeyboardpref: INTEGER_32 = 68 -- Declared in Windows as SPI_GETKEYBOARDPREF -- (from WEL_SPI_CONSTANTS) Spi_getkeyboardspeed: INTEGER_32 = 10 -- Declared in Windows as SPI_GETKEYBOARDSPEED -- (from WEL_SPI_CONSTANTS) Spi_getlowpoweractive: INTEGER_32 = 83 -- Declared in Windows as SPI_GETLOWPOWERACTIVE -- (from WEL_SPI_CONSTANTS) Spi_getlowpowertimeout: INTEGER_32 = 79 -- Declared in Windows as SPI_GETLOWPOWERTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getmenudropalignment: INTEGER_32 = 27 -- Declared in Windows as SPI_GETMENUDROPALIGNMENT -- (from WEL_SPI_CONSTANTS) Spi_getminimizedmetrics: INTEGER_32 = 43 -- Declared in Windows as SPI_GETMINIMIZEDMETRICS -- (from WEL_SPI_CONSTANTS) Spi_getmouse: INTEGER_32 = 3 -- Declared in Windows as SPI_GETMOUSE -- (from WEL_SPI_CONSTANTS) Spi_getmousekeys: INTEGER_32 = 54 -- Declared in Windows as SPI_GETMOUSEKEYS -- (from WEL_SPI_CONSTANTS) Spi_getmousetrails: INTEGER_32 = 94 -- Declared in Windows as SPI_GETMOUSETRAILS -- (from WEL_SPI_CONSTANTS) Spi_getnonclientmetrics: INTEGER_32 = 41 -- Declared in Windows as SPI_GETNONCLIENTMETRICS -- (from WEL_SPI_CONSTANTS) Spi_getpoweroffactive: INTEGER_32 = 84 -- Declared in Windows as SPI_GETPOWEROFFACTIVE -- (from WEL_SPI_CONSTANTS) Spi_getpowerofftimeout: INTEGER_32 = 80 -- Declared in Windows as SPI_GETPOWEROFFTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getscreenreader: INTEGER_32 = 70 -- Declared in Windows as SPI_GETSCREENREADER -- (from WEL_SPI_CONSTANTS) Spi_getscreensaveactive: INTEGER_32 = 16 -- Declared in Windows as SPI_GETSCREENSAVEACTIVE -- (from WEL_SPI_CONSTANTS) Spi_getscreensavetimeout: INTEGER_32 = 14 -- Declared in Windows as SPI_GETSCREENSAVETIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getserialkeys: INTEGER_32 = 62 -- Declared in Windows as SPI_GETSERIALKEYS -- (from WEL_SPI_CONSTANTS) Spi_getshowsounds: INTEGER_32 = 56 -- Declared in Windows as SPI_GETSHOWSOUNDS -- (from WEL_SPI_CONSTANTS) Spi_getsnaptodefbutton: INTEGER_32 = 95 -- Declared in Windows as SPI_GETSNAPTODEFBUTTON -- (from WEL_SPI_CONSTANTS) Spi_getsoundsentry: INTEGER_32 = 64 -- Declared in Windows as SPI_GETSOUNDSENTRY -- (from WEL_SPI_CONSTANTS) Spi_getstickykeys: INTEGER_32 = 58 -- Declared in Windows as SPI_GETSTICKYKEYS -- (from WEL_SPI_CONSTANTS) Spi_gettogglekeys: INTEGER_32 = 52 -- Declared in Windows as SPI_GETTOGGLEKEYS -- (from WEL_SPI_CONSTANTS) Spi_getwindowsextension: INTEGER_32 = 92 -- Declared in Windows as SPI_GETWINDOWSEXTENSION -- (from WEL_SPI_CONSTANTS) Spi_getworkarea: INTEGER_32 = 48 -- Declared in Windows as SPI_GETWORKAREA -- (from WEL_SPI_CONSTANTS) Spi_iconhorizontalspacing: INTEGER_32 = 13 -- Declared in Windows as SPI_ICONHORIZONTALSPACING -- (from WEL_SPI_CONSTANTS) Spi_iconverticalspacing: INTEGER_32 = 24 -- Declared in Windows as SPI_ICONVERTICALSPACING -- (from WEL_SPI_CONSTANTS) Spi_langdriver: INTEGER_32 = 12 -- Declared in Windows as SPI_LANGDRIVER -- (from WEL_SPI_CONSTANTS) Spi_screensaverrunning: INTEGER_32 = 97 -- Declared in Windows as SPI_SCREENSAVERRUNNING -- (from WEL_SPI_CONSTANTS) Spi_setaccesstimeout: INTEGER_32 = 61 -- Declared in Windows as SPI_SETACCESSTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setanimation: INTEGER_32 = 73 -- Declared in Windows as SPI_SETANIMATION -- (from WEL_SPI_CONSTANTS) Spi_setbeep: INTEGER_32 = 2 -- Declared in Windows as SPI_SETBEEP -- (from WEL_SPI_CONSTANTS) Spi_setborder: INTEGER_32 = 6 -- Declared in Windows as SPI_SETBORDER -- (from WEL_SPI_CONSTANTS) Spi_setcursors: INTEGER_32 = 87 -- Declared in Windows as SPI_SETCURSORS -- (from WEL_SPI_CONSTANTS) Spi_setdefaultinputlang: INTEGER_32 = 90 -- Declared in Windows as SPI_SETDEFAULTINPUTLANG -- (from WEL_SPI_CONSTANTS) Spi_setdeskpattern: INTEGER_32 = 21 -- Declared in Windows as SPI_SETDESKPATTERN -- (from WEL_SPI_CONSTANTS) Spi_setdeskwallpaper: INTEGER_32 = 20 -- Declared in Windows as SPI_SETDESKWALLPAPER -- (from WEL_SPI_CONSTANTS) Spi_setdoubleclicktime: INTEGER_32 = 32 -- Declared in Windows as SPI_SETDOUBLECLICKTIME -- (from WEL_SPI_CONSTANTS) Spi_setdoubleclkheight: INTEGER_32 = 30 -- Declared in Windows as SPI_SETDOUBLECLKHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_setdoubleclkwidth: INTEGER_32 = 29 -- Declared in Windows as SPI_SETDOUBLECLKWIDTH -- (from WEL_SPI_CONSTANTS) Spi_setdragfullwindows: INTEGER_32 = 37 -- Declared in Windows as SPI_SETDRAGFULLWINDOWS -- (from WEL_SPI_CONSTANTS) Spi_setdragheight: INTEGER_32 = 77 -- Declared in Windows as SPI_SETDRAGHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_setdragwidth: INTEGER_32 = 76 -- Declared in Windows as SPI_SETDRAGWIDTH -- (from WEL_SPI_CONSTANTS) Spi_setfasttaskswitch: INTEGER_32 = 36 -- Declared in Windows as SPI_SETFASTTASKSWITCH -- (from WEL_SPI_CONSTANTS) Spi_setfilterkeys: INTEGER_32 = 51 -- Declared in Windows as SPI_SETFILTERKEYS -- (from WEL_SPI_CONSTANTS) Spi_setfontsmoothing: INTEGER_32 = 75 -- Declared in Windows as SPI_SETFONTSMOOTHING -- (from WEL_SPI_CONSTANTS) Spi_setgridgranularity: INTEGER_32 = 19 -- Declared in Windows as SPI_SETGRIDGRANULARITY -- (from WEL_SPI_CONSTANTS) Spi_sethandheld: INTEGER_32 = 78 -- Declared in Windows as SPI_SETHANDHELD -- (from WEL_SPI_CONSTANTS) Spi_sethighcontrast: INTEGER_32 = 67 -- Declared in Windows as SPI_SETHIGHCONTRAST -- (from WEL_SPI_CONSTANTS) Spi_seticonmetrics: INTEGER_32 = 46 -- Declared in Windows as SPI_SETICONMETRICS -- (from WEL_SPI_CONSTANTS) Spi_seticons: INTEGER_32 = 88 -- Declared in Windows as SPI_SETICONS -- (from WEL_SPI_CONSTANTS) Spi_seticontitlelogfont: INTEGER_32 = 34 -- Declared in Windows as SPI_SETICONTITLELOGFONT -- (from WEL_SPI_CONSTANTS) Spi_seticontitlewrap: INTEGER_32 = 26 -- Declared in Windows as SPI_SETICONTITLEWRAP -- (from WEL_SPI_CONSTANTS) Spi_setkeyboarddelay: INTEGER_32 = 23 -- Declared in Windows as SPI_SETKEYBOARDDELAY -- (from WEL_SPI_CONSTANTS) Spi_setkeyboardpref: INTEGER_32 = 69 -- Declared in Windows as SPI_SETKEYBOARDPREF -- (from WEL_SPI_CONSTANTS) Spi_setkeyboardspeed: INTEGER_32 = 11 -- Declared in Windows as SPI_SETKEYBOARDSPEED -- (from WEL_SPI_CONSTANTS) Spi_setlangtoggle: INTEGER_32 = 91 -- Declared in Windows as SPI_SETLANGTOGGLE -- (from WEL_SPI_CONSTANTS) Spi_setlowpoweractive: INTEGER_32 = 85 -- Declared in Windows as SPI_SETLOWPOWERACTIVE -- (from WEL_SPI_CONSTANTS) Spi_setlowpowertimeout: INTEGER_32 = 81 -- Declared in Windows as SPI_SETLOWPOWERTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setmenudropalignment: INTEGER_32 = 28 -- Declared in Windows as SPI_SETMENUDROPALIGNMENT -- (from WEL_SPI_CONSTANTS) Spi_setminimizedmetrics: INTEGER_32 = 44 -- Declared in Windows as SPI_SETMINIMIZEDMETRICS -- (from WEL_SPI_CONSTANTS) Spi_setmouse: INTEGER_32 = 4 -- Declared in Windows as SPI_SETMOUSE -- (from WEL_SPI_CONSTANTS) Spi_setmousebuttonswap: INTEGER_32 = 33 -- Declared in Windows as SPI_SETMOUSEBUTTONSWAP -- (from WEL_SPI_CONSTANTS) Spi_setmousekeys: INTEGER_32 = 55 -- Declared in Windows as SPI_SETMOUSEKEYS -- (from WEL_SPI_CONSTANTS) Spi_setmousetrails: INTEGER_32 = 93 -- Declared in Windows as SPI_SETMOUSETRAILS -- (from WEL_SPI_CONSTANTS) Spi_setnonclientmetrics: INTEGER_32 = 42 -- Declared in Windows as SPI_SETNONCLIENTMETRICS -- (from WEL_SPI_CONSTANTS) Spi_setpenwindows: INTEGER_32 = 49 -- Declared in Windows as SPI_SETPENWINDOWS -- (from WEL_SPI_CONSTANTS) Spi_setpoweroffactive: INTEGER_32 = 86 -- Declared in Windows as SPI_SETPOWEROFFACTIVE -- (from WEL_SPI_CONSTANTS) Spi_setpowerofftimeout: INTEGER_32 = 82 -- Declared in Windows as SPI_SETPOWEROFFTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setscreenreader: INTEGER_32 = 71 -- Declared in Windows as SPI_SETSCREENREADER -- (from WEL_SPI_CONSTANTS) Spi_setscreensaveactive: INTEGER_32 = 17 -- Declared in Windows as SPI_SETSCREENSAVEACTIVE -- (from WEL_SPI_CONSTANTS) Spi_setscreensaverrunning: INTEGER_32 = 97 -- Declared in Windows as SPI_SETSCREENSAVERRUNNING -- (from WEL_SPI_CONSTANTS) Spi_setscreensavetimeout: INTEGER_32 = 15 -- Declared in Windows as SPI_SETSCREENSAVETIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setserialkeys: INTEGER_32 = 63 -- Declared in Windows as SPI_SETSERIALKEYS -- (from WEL_SPI_CONSTANTS) Spi_setshowsounds: INTEGER_32 = 57 -- Declared in Windows as SPI_SETSHOWSOUNDS -- (from WEL_SPI_CONSTANTS) Spi_setsnaptodefbutton: INTEGER_32 = 96 -- Declared in Windows as SPI_SETSNAPTODEFBUTTON -- (from WEL_SPI_CONSTANTS) Spi_setsoundsentry: INTEGER_32 = 65 -- Declared in Windows as SPI_SETSOUNDSENTRY -- (from WEL_SPI_CONSTANTS) Spi_setstickykeys: INTEGER_32 = 59 -- Declared in Windows as SPI_SETSTICKYKEYS -- (from WEL_SPI_CONSTANTS) Spi_settogglekeys: INTEGER_32 = 53 -- Declared in Windows as SPI_SETTOGGLEKEYS -- (from WEL_SPI_CONSTANTS) Spi_setworkarea: INTEGER_32 = 47 -- Declared in Windows as SPI_SETWORKAREA -- (from WEL_SPI_CONSTANTS) feature -- SystemParameter (Windows 98, Windows 2000 and above) Spi_getactivewindowtracking: INTEGER_32 = 4096 -- Declared in Windows as SPI_GETACTIVEWINDOWTRACKING -- (from WEL_SPI_CONSTANTS) Spi_getactivewndtrktimeout: INTEGER_32 = 8194 -- Declared in Windows as SPI_GETACTIVEWNDTRKTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getactivewndtrkzorder: INTEGER_32 = 4108 -- Declared in Windows as SPI_GETACTIVEWNDTRKZORDER -- (from WEL_SPI_CONSTANTS) Spi_getcaretwidth: INTEGER_32 = 8198 -- Declared in Windows as SPI_GETCARETWIDTH -- (from WEL_SPI_CONSTANTS) Spi_getcomboboxanimation: INTEGER_32 = 4100 -- Declared in Windows as SPI_GETCOMBOBOXANIMATION -- (from WEL_SPI_CONSTANTS) Spi_getcursorshadow: INTEGER_32 = 4122 -- Declared in Windows as SPI_GETCURSORSHADOW -- (from WEL_SPI_CONSTANTS) Spi_getdeskwallpaper: INTEGER_32 = 115 -- Declared in Windows as SPI_GETDESKWALLPAPER -- (from WEL_SPI_CONSTANTS) Spi_getforegroundflashcount: INTEGER_32 = 8196 -- Declared in Windows as SPI_GETFOREGROUNDFLASHCOUNT -- (from WEL_SPI_CONSTANTS) Spi_getforegroundlocktimeout: INTEGER_32 = 8192 -- Declared in Windows as SPI_GETFOREGROUNDLOCKTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_getgradientcaptions: INTEGER_32 = 4104 -- Declared in Windows as SPI_GETGRADIENTCAPTIONS -- (from WEL_SPI_CONSTANTS) Spi_gethottracking: INTEGER_32 = 4110 -- Declared in Windows as SPI_GETHOTTRACKING -- (from WEL_SPI_CONSTANTS) Spi_getkeyboardcues: INTEGER_32 = 4106 -- Declared in Windows as SPI_GETKEYBOARDCUES -- (from WEL_SPI_CONSTANTS) Spi_getlistboxsmoothscrolling: INTEGER_32 = 4102 -- Declared in Windows as SPI_GETLISTBOXSMOOTHSCROLLING -- (from WEL_SPI_CONSTANTS) Spi_getmenuanimation: INTEGER_32 = 4098 -- Declared in Windows as SPI_GETMENUANIMATION -- (from WEL_SPI_CONSTANTS) Spi_getmenufade: INTEGER_32 = 4114 -- Declared in Windows as SPI_GETMENUFADE -- (from WEL_SPI_CONSTANTS) Spi_getmenuunderlines: INTEGER_32 = 4106 -- Declared in Windows as SPI_GETMENUUNDERLINES -- (from WEL_SPI_CONSTANTS) Spi_getmousespeed: INTEGER_32 = 112 -- Declared in Windows as SPI_GETMOUSESPEED -- (from WEL_SPI_CONSTANTS) Spi_getscreensaverrunning: INTEGER_32 = 114 -- Declared in Windows as SPI_GETSCREENSAVERRUNNING -- (from WEL_SPI_CONSTANTS) Spi_getselectionfade: INTEGER_32 = 4116 -- Declared in Windows as SPI_GETSELECTIONFADE -- (from WEL_SPI_CONSTANTS) Spi_gettooltipanimation: INTEGER_32 = 4118 -- Declared in Windows as SPI_GETTOOLTIPANIMATION -- (from WEL_SPI_CONSTANTS) Spi_gettooltipfade: INTEGER_32 = 4120 -- Declared in Windows as SPI_GETTOOLTIPFADE -- (from WEL_SPI_CONSTANTS) Spi_getuieffects: INTEGER_32 = 4158 -- Declared in Windows as SPI_GETUIEFFECTS -- (from WEL_SPI_CONSTANTS) Spi_setactivewindowtracking: INTEGER_32 = 4097 -- Declared in Windows as SPI_SETACTIVEWINDOWTRACKING -- (from WEL_SPI_CONSTANTS) Spi_setactivewndtrktimeout: INTEGER_32 = 8195 -- Declared in Windows as SPI_SETACTIVEWNDTRKTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setactivewndtrkzorder: INTEGER_32 = 4109 -- Declared in Windows as SPI_SETACTIVEWNDTRKZORDER -- (from WEL_SPI_CONSTANTS) Spi_setcaretwidth: INTEGER_32 = 8199 -- Declared in Windows as SPI_SETCARETWIDTH -- (from WEL_SPI_CONSTANTS) Spi_setcomboboxanimation: INTEGER_32 = 4101 -- Declared in Windows as SPI_SETCOMBOBOXANIMATION -- (from WEL_SPI_CONSTANTS) Spi_setcursorshadow: INTEGER_32 = 4123 -- Declared in Windows as SPI_SETCURSORSHADOW -- (from WEL_SPI_CONSTANTS) Spi_setforegroundflashcount: INTEGER_32 = 8197 -- Declared in Windows as SPI_SETFOREGROUNDFLASHCOUNT -- (from WEL_SPI_CONSTANTS) Spi_setforegroundlocktimeout: INTEGER_32 = 8193 -- Declared in Windows as SPI_SETFOREGROUNDLOCKTIMEOUT -- (from WEL_SPI_CONSTANTS) Spi_setgradientcaptions: INTEGER_32 = 4105 -- Declared in Windows as SPI_SETGRADIENTCAPTIONS -- (from WEL_SPI_CONSTANTS) Spi_sethottracking: INTEGER_32 = 4111 -- Declared in Windows as SPI_SETHOTTRACKING -- (from WEL_SPI_CONSTANTS) Spi_setkeyboardcues: INTEGER_32 = 4107 -- Declared in Windows as SPI_SETKEYBOARDCUES -- (from WEL_SPI_CONSTANTS) Spi_setlistboxsmoothscrolling: INTEGER_32 = 4103 -- Declared in Windows as SPI_SETLISTBOXSMOOTHSCROLLING -- (from WEL_SPI_CONSTANTS) Spi_setmenuanimation: INTEGER_32 = 4099 -- Declared in Windows as SPI_SETMENUANIMATION -- (from WEL_SPI_CONSTANTS) Spi_setmenufade: INTEGER_32 = 4115 -- Declared in Windows as SPI_SETMENUFADE -- (from WEL_SPI_CONSTANTS) Spi_setmenuunderlines: INTEGER_32 = 4107 -- Declared in Windows as SPI_SETMENUUNDERLINES -- (from WEL_SPI_CONSTANTS) Spi_setmousespeed: INTEGER_32 = 113 -- Declared in Windows as SPI_SETMOUSESPEED -- (from WEL_SPI_CONSTANTS) Spi_setselectionfade: INTEGER_32 = 4117 -- Declared in Windows as SPI_SETSELECTIONFADE -- (from WEL_SPI_CONSTANTS) Spi_settooltipanimation: INTEGER_32 = 4119 -- Declared in Windows as SPI_SETTOOLTIPANIMATION -- (from WEL_SPI_CONSTANTS) Spi_settooltipfade: INTEGER_32 = 4121 -- Declared in Windows as SPI_SETTOOLTIPFADE -- (from WEL_SPI_CONSTANTS) Spi_setuieffects: INTEGER_32 = 4159 -- Declared in Windows as SPI_SETUIEFFECTS -- (from WEL_SPI_CONSTANTS) feature -- SystemParameter (Windows NT 4.0, Windows 98, Windows 2000 and above) Spi_getmenushowdelay: INTEGER_32 = 106 -- Declared in Windows as SPI_GETMENUSHOWDELAY -- (from WEL_SPI_CONSTANTS) Spi_getmousehoverheight: INTEGER_32 = 100 -- Declared in Windows as SPI_GETMOUSEHOVERHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_getmousehovertime: INTEGER_32 = 102 -- Declared in Windows as SPI_GETMOUSEHOVERTIME -- (from WEL_SPI_CONSTANTS) Spi_getmousehoverwidth: INTEGER_32 = 98 -- Declared in Windows as SPI_GETMOUSEHOVERWIDTH -- (from WEL_SPI_CONSTANTS) Spi_getshowimeui: INTEGER_32 = 110 -- Declared in Windows as SPI_GETSHOWIMEUI -- (from WEL_SPI_CONSTANTS) Spi_getwheelscrolllines: INTEGER_32 = 104 -- Declared in Windows as SPI_GETWHEELSCROLLLINES -- (from WEL_SPI_CONSTANTS) Spi_setmenushowdelay: INTEGER_32 = 107 -- Declared in Windows as SPI_SETMENUSHOWDELAY -- (from WEL_SPI_CONSTANTS) Spi_setmousehoverheight: INTEGER_32 = 101 -- Declared in Windows as SPI_SETMOUSEHOVERHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_setmousehovertime: INTEGER_32 = 103 -- Declared in Windows as SPI_SETMOUSEHOVERTIME -- (from WEL_SPI_CONSTANTS) Spi_setmousehoverwidth: INTEGER_32 = 99 -- Declared in Windows as SPI_SETMOUSEHOVERWIDTH -- (from WEL_SPI_CONSTANTS) Spi_setshowimeui: INTEGER_32 = 111 -- Declared in Windows as SPI_SETSHOWIMEUI -- (from WEL_SPI_CONSTANTS) Spi_setwheelscrolllines: INTEGER_32 = 105 -- Declared in Windows as SPI_SETWHEELSCROLLLINES -- (from WEL_SPI_CONSTANTS) feature -- SystemParameter (Windows XP and above) Spi_getdropshadow: INTEGER_32 = 4132 -- Declared in Windows as SPI_GETDROPSHADOW -- (from WEL_SPI_CONSTANTS) Spi_getflatmenu: INTEGER_32 = 4130 -- Declared in Windows as SPI_GETFLATMENU -- (from WEL_SPI_CONSTANTS) Spi_getfocusborderheight: INTEGER_32 = 8208 -- Declared in Windows as SPI_GETFOCUSBORDERHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_getfocusborderwidth: INTEGER_32 = 8206 -- Declared in Windows as SPI_GETFOCUSBORDERWIDTH -- (from WEL_SPI_CONSTANTS) Spi_getfontsmoothingcontrast: INTEGER_32 = 8204 -- Declared in Windows as SPI_GETFONTSMOOTHINGCONTRAST -- (from WEL_SPI_CONSTANTS) Spi_getfontsmoothingtype: INTEGER_32 = 8202 -- Declared in Windows as SPI_GETFONTSMOOTHINGTYPE -- (from WEL_SPI_CONSTANTS) Spi_getmouseclicklock: INTEGER_32 = 4126 -- Declared in Windows as SPI_GETMOUSECLICKLOCK -- (from WEL_SPI_CONSTANTS) Spi_getmouseclicklocktime: INTEGER_32 = 8200 -- Declared in Windows as SPI_GETMOUSECLICKLOCKTIME -- (from WEL_SPI_CONSTANTS) Spi_getmousesonar: INTEGER_32 = 4124 -- Declared in Windows as SPI_GETMOUSESONAR -- (from WEL_SPI_CONSTANTS) Spi_getmousevanish: INTEGER_32 = 4128 -- Declared in Windows as SPI_GETMOUSEVANISH -- (from WEL_SPI_CONSTANTS) Spi_setdropshadow: INTEGER_32 = 4133 -- Declared in Windows as SPI_SETDROPSHADOW -- (from WEL_SPI_CONSTANTS) Spi_setflatmenu: INTEGER_32 = 4131 -- Declared in Windows as SPI_SETFLATMENU -- (from WEL_SPI_CONSTANTS) Spi_setfocusborderheight: INTEGER_32 = 8209 -- Declared in Windows as SPI_SETFOCUSBORDERHEIGHT -- (from WEL_SPI_CONSTANTS) Spi_setfocusborderwidth: INTEGER_32 = 8207 -- Declared in Windows as SPI_SETFOCUSBORDERWIDTH -- (from WEL_SPI_CONSTANTS) Spi_setfontsmoothingcontrast: INTEGER_32 = 8205 -- Declared in Windows as SPI_SETFONTSMOOTHINGCONTRAST -- (from WEL_SPI_CONSTANTS) Spi_setfontsmoothingtype: INTEGER_32 = 8203 -- Declared in Windows as SPI_SETFONTSMOOTHINGTYPE -- (from WEL_SPI_CONSTANTS) Spi_setmouseclicklock: INTEGER_32 = 4127 -- Declared in Windows as SPI_SETMOUSECLICKLOCK -- (from WEL_SPI_CONSTANTS) Spi_setmouseclicklocktime: INTEGER_32 = 8201 -- Declared in Windows as SPI_SETMOUSECLICKLOCKTIME -- (from WEL_SPI_CONSTANTS) Spi_setmousesonar: INTEGER_32 = 4125 -- Declared in Windows as SPI_SETMOUSESONAR -- (from WEL_SPI_CONSTANTS) Spi_setmousevanish: INTEGER_32 = 4129 -- Declared in Windows as SPI_SETMOUSEVANISH -- (from WEL_SPI_CONSTANTS) feature -- SystemParameterInfo Flags (all Windows) Spif_sendchange: INTEGER_32 = 2 -- Declared in Windows as SPIF_SENDCHANGE -- (from WEL_SPI_CONSTANTS) Spif_sendwininichange: INTEGER_32 = 2 -- Declared in Windows as SPIF_SENDWININICHANGE -- (from WEL_SPI_CONSTANTS) Spif_updateinifile: INTEGER_32 = 1 -- Declared in Windows as SPIF_UPDATEINIFILE -- (from WEL_SPI_CONSTANTS) feature -- Version Constants Version_400: INTEGER_32 = 262144 -- version_400 <=> Microsoft Windows 95/Windows NT 4.0 -- (from WEL_WINDOWS_VERSION) Version_470: INTEGER_32 = 262214 -- version_470 <=> Microsoft Internet Explorer 3.x -- (from WEL_WINDOWS_VERSION) Version_471: INTEGER_32 = 262215 -- version_471 <=> Microsoft Internet Explorer 4.0 -- (from WEL_WINDOWS_VERSION) Version_472: INTEGER_32 = 262216 -- version_472 <=> Microsoft Internet Explorer 4.01 & Windows 98 -- (from WEL_WINDOWS_VERSION) Version_500: INTEGER_32 = 327680 -- version_500 (Shlwapi.dll) <=> Microsoft Internet Explorer 5 -- version_500 (Shell32.dll) <=> Microsoft Windows 2000 -- (from WEL_WINDOWS_VERSION) Version_580: INTEGER_32 = 327760 -- version_580 (Comctl32.dll) <=> Microsoft Internet Explorer 5 -- (from WEL_WINDOWS_VERSION) Version_581: INTEGER_32 = 327761 -- version_581 (Comctl32.dll)<=> Microsoft Windows 2000 -- (from WEL_WINDOWS_VERSION) Version_600: INTEGER_32 = 393216 -- version_600 (Comctl32.dll)<=> Microsoft Windows XP -- (from WEL_WINDOWS_VERSION) feature -- Windows Versions (output) version_number_string: STRING_8 -- String representing the version number using the following format -- <major_version>.<minor_version>.<build_number> for Windows NT, 2000, XP -- <major_version>.<minor_version> for Windows 95, 98, Me -- (from WEL_WINDOWS_VERSION) invariant -- from EV_PICK_AND_DROPABLE_I user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1 pebble_function_takes_two_integer_open_operands: attached pebble_function as l_pebble_function implies l_pebble_function.valid_operands ([1, 1]) -- from EV_ANY_I interface_coupled: is_usable implies interface /= Void and then attached_interface.implementation = Current base_make_called: is_usable implies base_make_called -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from EV_POSITIONED_I minimum_width_positive_or_zero: is_usable implies minimum_width >= 0 minimum_height_positive_or_zero: is_usable implies minimum_height >= 0 -- from EV_DYNAMIC_LIST_I index_within_bounds: is_usable implies (index >= 0 and then index <= count + 1) -- from EV_ID_IMP make_called: id > 0 note copyright: "Copyright (c) 1984-2017, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class EV_MENU_IMP -- Generated by Eiffel Studio --
For more details: eiffel.org