indexing
description: "Screen device context."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
WEL_SCREEN_DC
create
default_create
ANY
feature
bitmap: WEL_BITMAP
WEL_DC
brush: WEL_BRUSH
WEL_DC
font: WEL_FONT
WEL_DC
generating_type: STRING_8
ANY
generator: STRING_8
ANY
item: POINTER
WEL_ANY
palette: WEL_PALETTE
WEL_DC
pen: WEL_PEN
WEL_DC
region: WEL_REGION
WEL_DC
feature
frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies some.same_type (other)
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
background_color: WEL_COLOR_REF
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
bitmap_selected: BOOLEAN
WEL_DC
brush_selected: BOOLEAN
WEL_DC
char_abc_widths (first_char_index, last_char_index: NATURAL_32): ARRAYED_LIST [WEL_ABC_STRUCT]
`Result'
`first_char_index'`last_char_index'
WEL_DC
require WEL_DC
indexes_valid: first_char_index >= 1 and last_char_index >= first_char_index
valid_range: (last_char_index - first_char_index) <= {INTEGER_32}.max_value.to_natural_32
ensure WEL_DC
result_not_void: Result /= Void
character_size (c: CHARACTER_8): WEL_SIZE
`s'
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_exists: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
device_caps (capability: INTEGER_32): INTEGER_32
`capability'
WEL_DC
require WEL_DC
exists: exists
exists: BOOLEAN
item
WEL_ANY
require WEL_REFERENCE_TRACKABLE
True
ensure WEL_ANY
Result = (item /= default_pointer)
font_selected: BOOLEAN
WEL_DC
height: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
is_opaque: BOOLEAN
WEL_DC
require WEL_DC
exists: exists
is_transparent: BOOLEAN
WEL_DC
require WEL_DC
exists: exists
map_mode: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
valid_map_mode: valid_map_mode_constant (Result)
mask_blt_supported: BOOLEAN
WEL_DC
palette_selected: BOOLEAN
WEL_DC
pen_selected: BOOLEAN
WEL_DC
pixel_color (x, y: INTEGER_32): WEL_COLOR_REF
`x'`y'
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
polygon_fill_mode: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
valid_polygon_fill_mode: valid_polygon_fill_mode_constant (Result)
position: WEL_POINT
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_exists: Result /= Void
region_selected: BOOLEAN
WEL_DC
rop2: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
valid_result: valid_rop2_constant (Result)
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
stretch_blt_mode: INTEGER_32
stretch_blt
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
valid_stretch_mode: valid_stretch_mode_constant (Result)
string_height (s: STRING_GENERAL): INTEGER_32
`s'
WEL_DC
require WEL_DC
exists: exists
s_exists: s /= Void
ensure WEL_DC
positive_result: Result >= 0
string_size (s: STRING_GENERAL): WEL_SIZE
`s'
WEL_DC
require WEL_DC
exists: exists
s_exists: s /= Void
ensure WEL_DC
result_exists: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
string_width (s: STRING_GENERAL): INTEGER_32
`s'
WEL_DC
require WEL_DC
exists: exists
s_exists: s /= Void
ensure WEL_DC
positive_result: Result >= 0
tabbed_text_height (text: STRING_GENERAL): INTEGER_32
`text'
WEL_DC
require WEL_DC
exists: exists
text_not_void: text /= Void
ensure WEL_DC
positive_height: Result >= 0
tabbed_text_size (text: STRING_GENERAL): WEL_SIZE
`text'
WEL_DC
require WEL_DC
exists: exists
text_not_void: text /= Void
ensure WEL_DC
result_not_void: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
tabbed_text_size_with_tabulation (text: STRING_GENERAL; tabulations: ARRAY [INTEGER_32]): WEL_SIZE
`text'`tabulations'
WEL_DC
require WEL_DC
exists: exists
text_not_void: text /= Void
tabulations_not_void: tabulations /= Void
ensure WEL_DC
result_not_void: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
tabbed_text_width (text: STRING_GENERAL): INTEGER_32
`text'
WEL_DC
require WEL_DC
exists: exists
text_not_void: text /= Void
ensure WEL_DC
positive_width: Result >= 0
text_alignment: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
text_color: WEL_COLOR_REF
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
text_face: STRING_GENERAL
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
valid_extent_map_mode (mode: INTEGER_32): BOOLEAN
`mode'
WEL_DC
require WEL_DC
valid_map_mode: valid_map_mode_constant (mode)
viewport_extent: WEL_SIZE
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
viewport_origin: WEL_POINT
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
width: INTEGER_32
WEL_DC
require WEL_DC
exists: exists
window_extent: WEL_SIZE
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
window_origin: WEL_POINT
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
result_not_void: Result /= Void
feature {ANY}
valid_dib_colors_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_DIB_COLORS_CONSTANTS
valid_htext_alignment_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_TA_CONSTANTS
valid_map_mode_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_MM_CONSTANTS
valid_polygon_fill_mode_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_POLYGON_FILL_MODE_CONSTANTS
valid_rop2_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_DRAWING_CONSTANTS
valid_stretch_mode_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_STRETCH_MODE_CONSTANTS
valid_text_alignment_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_TA_CONSTANTS
valid_vtext_alignment_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_TA_CONSTANTS
feature
select_bitmap (a_bitmap: WEL_BITMAP)
`a_bitmap'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
ensure WEL_DC
bitmap_set: bitmap = a_bitmap
bitmap_selected: bitmap_selected
select_brush (a_brush: WEL_BRUSH)
`a_brush'
WEL_DC
require WEL_DC
exists: exists
a_brush_not_void: a_brush /= Void
a_brush_exists: a_brush.exists
ensure WEL_DC
brush_set: brush = a_brush
brush_selected: brush_selected
select_font (a_font: WEL_FONT)
`a_font'
WEL_DC
require WEL_DC
exists: exists
a_font_not_void: a_font /= Void
a_font_exists: a_font.exists
ensure WEL_DC
font_set: font = a_font
font_selected: font_selected
select_palette (a_palette: WEL_PALETTE)
`a_palette'
WEL_DC
require WEL_DC
exists: exists
a_palette_not_void: a_palette /= Void
a_palette_exists: a_palette.exists
select_pen (a_pen: WEL_PEN)
`a_pen'
WEL_DC
require WEL_DC
exists: exists
a_pen_not_void: a_pen /= Void
a_pen_exists: a_pen.exists
ensure WEL_DC
pen_set: pen = a_pen
pen_selected: pen_selected
select_region (a_region: WEL_REGION)
`a_region'
WEL_DC
require WEL_DC
exists: exists
a_region_not_void: a_region /= Void
a_region_exists: a_region.exists
ensure WEL_DC
region_set: region = a_region
region_selected: region_selected
set_background_color (color: WEL_COLOR_REF)
background_color`color'
WEL_DC
require WEL_DC
exists: exists
color_not_void: color /= Void
ensure WEL_DC
color_set: background_color.item = color.item
set_background_opaque
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
is_opaque: is_opaque
set_background_transparent
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
is_transparent: is_transparent
set_di_bits (a_bitmap: WEL_BITMAP; start_scan, scan_lines: INTEGER_32; bits: ARRAY [CHARACTER_8]; bitmap_info: WEL_BITMAP_INFO; usage: INTEGER_32): INTEGER_32
`a_bitmap'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
positive_start_scan: start_scan >= 0
positive_scan_lines: scan_lines >= 0
bitmap_info_not_void: bitmap_info /= Void
valid_usage: valid_dib_colors_constant (usage)
set_hv_text_alignment (h, v: INTEGER_32)
`h'`v'
WEL_DC
require WEL_DC
exists: exists
valid_horizontal_alignment: valid_htext_alignment_constant (h)
valid_vertical_alignment: valid_vtext_alignment_constant (v)
ensure WEL_DC
text_alignments_set: flag_set (text_alignment, h) and flag_set (text_alignment, v)
set_map_mode (mode: INTEGER_32)
`mode'
`mode'
WEL_DC
require WEL_DC
exists: exists
valid_map_mode: valid_map_mode_constant (mode)
ensure WEL_DC
map_mode_set: map_mode = mode
set_polygon_fill_mode (mode: INTEGER_32)
polygon_fill_mode
`mode'
`mode'
WEL_DC
require WEL_DC
exists: exists
valid_polygon_fill_mode: valid_polygon_fill_mode_constant (mode)
ensure WEL_DC
polygon_fill_mode_set: polygon_fill_mode = mode
set_rop2 (a_rop2: INTEGER_32)
`a_rop2'
WEL_DC
require WEL_DC
exists: exists
valid_rop2_constant: valid_rop2_constant (a_rop2)
ensure WEL_DC
rop2_set: rop2 = a_rop2
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_stretch_blt_mode (a_mode: INTEGER_32)
`a_mode'
`a_mode'
WEL_DC
require WEL_DC
exists: exists
valid_stretch_mode_constant: valid_stretch_mode_constant (a_mode)
ensure WEL_DC
stretch_blt_mode_set: stretch_blt_mode = a_mode
set_text_alignment (an_alignment: INTEGER_32)
`an_alignment'
`an_alignment'
WEL_DC
require WEL_DC
exists: exists
valid_alignment: valid_text_alignment_constant (an_alignment)
ensure WEL_DC
text_alignment_set: flag_set (text_alignment, an_alignment)
set_text_color (color: WEL_COLOR_REF)
text_color`color'
WEL_DC
require WEL_DC
exists: exists
color_not_void: color /= Void
ensure WEL_DC
color_set: text_color.item = color.item
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
set_viewport_extent (x_extent, y_extent: INTEGER_32)
`x_extent'`y_extent'
WEL_DC
require WEL_DC
exists: exists
valid_current_map_mode: valid_extent_map_mode (map_mode)
ensure WEL_DC
x_viewport_extent_set: map_mode /= mm_isotropic implies viewport_extent.width = x_extent
y_viewport_extent_set: map_mode /= mm_isotropic implies viewport_extent.height = y_extent
set_viewport_origin (x_origin, y_origin: INTEGER_32)
`x_origin'`y_origin'
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
x_viewport_origin_set: viewport_origin.x = x_origin
y_viewport_origin_set: viewport_origin.y = y_origin
set_window_extent (x_extent, y_extent: INTEGER_32)
`x_extent'`y_extent'
WEL_DC
require WEL_DC
exists: exists
valid_current_map_mode: valid_extent_map_mode (map_mode)
ensure WEL_DC
x_window_extent_set: map_mode /= mm_isotropic implies window_extent.width = x_extent
y_window_extent_set: map_mode /= mm_isotropic implies window_extent.height = y_extent
set_window_origin (x_origin, y_origin: INTEGER_32)
`x_origin'`y_origin'
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
x_window_origin_set: window_origin.x = x_origin
y_window_origin_set: window_origin.y = y_origin
unselect_all
WEL_DC
require WEL_DC
exists: exists
ensure WEL_DC
pen_not_selected: not pen_selected
brush_not_selected: not brush_selected
region_not_selected: not region_selected
palette_not_selected: not palette_selected
font_not_selected: not font_selected
bitmap_not_selected: not bitmap_selected
unselect_bitmap
WEL_DC
require WEL_DC
exists: exists
bitmap_selected: bitmap_selected
ensure WEL_DC
bitmap_not_selected: not bitmap_selected
unselect_brush
WEL_DC
require WEL_DC
exists: exists
brush_selected: brush_selected
ensure WEL_DC
brush_not_selected: not brush_selected
unselect_font
WEL_DC
require WEL_DC
exists: exists
font_selected: font_selected
ensure WEL_DC
font_not_selected: not font_selected
unselect_palette
WEL_DC
require WEL_DC
exists: exists
palette_selected: palette_selected
ensure WEL_DC
palette_not_selected: not palette_selected
unselect_pen
WEL_DC
require WEL_DC
exists: exists
pen_selected: pen_selected
ensure WEL_DC
pen_not_selected: not pen_selected
unselect_region
WEL_DC
require WEL_DC
exists: exists
region_selected: region_selected
ensure WEL_DC
region_not_selected: not region_selected
feature
set_item (an_item: POINTER)
item`an_item'
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
feature
delete
`Current'
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
reference_not_tracked: not reference_tracked
ensure WEL_REFERENCE_TRACKABLE
destroyed: not shared implies not exists
dispose
`Current'
WEL_REFERENCE_TRACKABLE
require DISPOSABLE
True
ensure then WEL_REFERENCE_TRACKABLE
internal_object_id_freed: internal_object_id = 0
feature
copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: like Current)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: like Current
ANY
ensure ANY
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: like Current
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
alpha_blend (a_x_dest, a_y_dest, a_width, a_height: INTEGER_32; a_dc_src: WEL_DC; a_x_src, a_y_src, a_width_src, a_height_src: INTEGER_32; a_blend_function: WEL_BLEND_FUNCTION): BOOLEAN
WEL_DC
require WEL_DC
exists: exists
arc (left, top, right, bottom, x_start_arc, y_start_arc, x_end_arc, y_end_arc: INTEGER_32)
`left'`top'`right'`bottom'
`x_start_arc'`y_start_arc'
`x_end_arc'`y_end_arc'
WEL_DC
require WEL_DC
exists: exists
bit_blt (x_destination, y_destination, a_width, a_height: INTEGER_32; dc_source: WEL_DC; x_source, y_source, raster_operation: INTEGER_32)
`dc_source'
`x_source'
`y_source'`x_destination'`y_destination'
`a_width'`a_height'`raster_operation'
`raster_operation'
WEL_DC
require WEL_DC
exists: exists
positive_width: a_width >= 0
positive_height: a_height >= 0
dc_source_not_void: dc_source /= Void
dc_source_exists: dc_source.exists
chord (left, top, right, bottom, x_start_line, y_start_line, x_end_line, y_end_line: INTEGER_32)
`left'`top'`right'`bottom'
`x_start_line'`y_start_line'
`x_end_line'`y_end_line'
WEL_DC
require WEL_DC
exists: exists
copy_dc (dc_source: WEL_DC; rect: WEL_RECT)
`rect'`dc_source'
WEL_DC
require WEL_DC
exists: exists
rect_not_void: rect /= Void
dc_source_not_void: dc_source /= Void
dc_source_exists: dc_source.exists
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
di_bits (a_bitmap: WEL_BITMAP; start_scan, scan_lines: INTEGER_32; bitmap_info: WEL_BITMAP_INFO; usage: INTEGER_32): ARRAY [CHARACTER_8]
`a_bitmap'
`start_scan'
`scan_lines'
`bitmap_info'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
positive_start_scan: start_scan >= 0
positive_scan_lines: scan_lines >= 0
bitmap_info_not_void: bitmap_info /= Void
valid_usage: valid_dib_colors_constant (usage)
ensure WEL_DC
result_not_void: Result /= Void
consistent_count: Result.count = bitmap_info.header.size_image
frozen do_nothing
ANY
draw_bitmap (a_bitmap: WEL_BITMAP; x, y, a_width, a_height: INTEGER_32)
bitmap`x'`y'
`a_width'`a_height'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
draw_bitmap_with_raster_operation (a_bitmap: WEL_BITMAP; x, y, a_width, a_height, raster_operation: INTEGER_32)
bitmap`raster_operation'`x'`y'
`a_width'`a_height'
`raster_operation'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
draw_centered_text (string: STRING_GENERAL; rect: WEL_RECT)
`string'`rect'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
rect_not_void: rect /= Void
draw_cursor (cursor: WEL_CURSOR; x, y: INTEGER_32)
`cursor'`x'`y'
WEL_DC
require WEL_DC
exists: exists
cursor_not_void: cursor /= Void
cursor_exists: cursor.exists
draw_disabled_text (string: STRING_GENERAL; rect: WEL_RECT; format: INTEGER_32)
`string'
`rect'`format'
`format'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
rect_not_void: rect /= Void
draw_edge (a_rect: WEL_RECT; edge_type: INTEGER_32; edge_border: INTEGER_32)
`edge_type'
`edge_border'`a_rect'
`edge_type'
`edge_type'
WEL_DC
require WEL_DC
exists: exists
valid_rect: a_rect /= Void and then a_rect.exists
draw_frame_control (a_rect: WEL_RECT; control_type: INTEGER_32; control_state: INTEGER_32)
`control_type'
`control_state'
`control_type'
`control_state'
WEL_DC
require WEL_DC
exists: exists
valid_rect: a_rect /= Void and then a_rect.exists
draw_icon (icon: WEL_ICON; x, y: INTEGER_32)
`icon'`x'`y'
WEL_DC
require WEL_DC
exists: exists
icon_not_void: icon /= Void
icon_exists: icon.exists
draw_icon_ex (icon: WEL_ICON; x, y, icon_width, icon_height, frame_index: INTEGER_32; flicker_free_background: WEL_BRUSH; di_flags: INTEGER_32)
`icon'`x'`y'
WEL_DC
require WEL_DC
exists: exists
icon_not_void: icon /= Void
icon_exists: icon.exists
draw_state_bitmap (a_brush: WEL_BRUSH; a_bitmap: WEL_BITMAP; x, y: INTEGER_32; format: INTEGER_32)
`a_bitmap'`format'
`x'`y'`a_brush'`format'Dss_mono
`format'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
draw_state_icon (a_brush: WEL_BRUSH; an_icon: WEL_GRAPHICAL_RESOURCE; x, y: INTEGER_32; format: INTEGER_32)
`an_icon'`format'
`x'`y'`a_brush'`format'Dss_mono
`format'
WEL_DC
require WEL_DC
exists: exists
an_icon_not_void: an_icon /= Void
draw_state_text (a_brush: WEL_BRUSH; string: STRING_GENERAL; x, y: INTEGER_32; format: INTEGER_32)
`string'`format'
`x'`y'`a_brush'`format'Dss_mono
`format'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
draw_text (string: STRING_GENERAL; rect: WEL_RECT; format: INTEGER_32)
`string'
`rect'`format'
`format'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
rect_not_void: rect /= Void
draw_text_with_result (string: STRING_GENERAL; rect: WEL_RECT; format: INTEGER_32): INTEGER_32
`string'`rect'`format'
`format'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
rect_not_void: rect /= Void
ellipse (left, top, right, bottom: INTEGER_32)
`left'`top'`right'`bottom'
WEL_DC
require WEL_DC
exists: exists
fill_rect (a_rect: WEL_RECT; a_brush: WEL_BRUSH)
`a_rect'`a_brush'
WEL_DC
require WEL_DC
exists: exists
a_rect_not_void: a_rect /= Void
a_brush_not_void: a_brush /= Void
a_brush_exists: a_brush.exists
fill_region (a_region: WEL_REGION; a_brush: WEL_BRUSH)
`a_region'`a_brush'
WEL_DC
require WEL_DC
exists: exists
a_region_not_void: a_region /= Void
a_brush_not_void: a_brush /= Void
a_brush_exists: a_brush.exists
flood_fill_border (x, y: INTEGER_32; color: WEL_COLOR_REF)
`color'
`x'`y'
WEL_DC
require WEL_DC
exists: exists
color_not_void: color /= Void
flood_fill_surface (x, y: INTEGER_32; color: WEL_COLOR_REF)
`color'
`x'`y'
WEL_DC
require WEL_DC
exists: exists
color_not_void: color /= Void
get
invert_rect (a_rect: WEL_RECT)
`a_rect'
WEL_DC
require WEL_DC
exists: exists
a_rect_not_void: a_rect /= Void
invert_region (a_region: WEL_REGION)
`a_region'
WEL_DC
require WEL_DC
exists: exists
a_region_not_void: a_region /= Void
a_region_exists: a_region.exists
line (x1, y1, x2, y2: INTEGER_32)
`x1'`y1'`x2'`y2'
WEL_DC
require WEL_DC
exists: exists
line_to (x, y: INTEGER_32)
`x'`y'
WEL_DC
require WEL_DC
exists: exists
make_rop4 (fore, back: INTEGER_32): INTEGER_32
`Result'
`fore'`back'`raster_operation'
mask_blt
WEL_DC
mask_blt (x_destination, y_destination, a_width, a_height: INTEGER_32; dc_source: WEL_DC; x_source, y_source: INTEGER_32; mask_bitmap: WEL_BITMAP; x_mask, y_mask, raster_operation: INTEGER_32)
`raster_operation'
WEL_DC
require WEL_DC
exists: exists
positive_width: a_width >= 0
positive_height: a_height >= 0
mask_bitmap_not_void: mask_bitmap /= Void
function_is_supported: mask_blt_supported
move_to (x, y: INTEGER_32)
`x'`y'
WEL_DC
require WEL_DC
exists: exists
pat_blt (x_destination, y_destination, a_width, a_height: INTEGER_32; raster_operation: INTEGER_32)
`x_destination'
`y_destination'`a_width'`a_height'
`raster_operation'
`raster_operation'
WEL_DC
require WEL_DC
exists: exists
positive_width: a_width >= 0
positive_height: a_height >= 0
pie (left, top, right, bottom, x_start_point, y_start_point, x_end_point, y_end_point: INTEGER_32)
`left'`top'`right'`bottom'
`x_start_point'`y_start_point'
`x_end_point'`y_end_point'
WEL_DC
require WEL_DC
exists: exists
poly_bezier (points: ARRAY [INTEGER_32])
`points'
WEL_DC
require WEL_DC
points_not_void: points /= Void
points_count_ok: points.count \\ 2 = 0
poly_bezier_to (points: ARRAY [INTEGER_32])
`points'
WEL_DC
require WEL_DC
points_not_void: points /= Void
points_count_ok: points.count \\ 2 = 0
polygon (points: ARRAY [INTEGER_32])
`points'
WEL_DC
require WEL_DC
exists: exists
points_not_void: points /= Void
points_count: points.count \\ 2 = 0
polyline (points: ARRAY [INTEGER_32])
`points'
WEL_DC
require WEL_DC
exists: exists
points_not_void: points /= Void
points_count: points.count \\ 2 = 0
quick_release
require WEL_DISPLAY_DC
exists: exists
no_selected_pen: not pen_selected
no_selected_brush: not brush_selected
no_selected_bitmap: not bitmap_selected
no_selected_font: not font_selected
ensure then WEL_DISPLAY_DC
not_exists: not exists
realize_palette
WEL_DC
require WEL_DC
exists: exists
palette_selected: palette_selected
rectangle (left, top, right, bottom: INTEGER_32)
`left'`top'
`right'`bottom'
WEL_DC
require WEL_DC
exists: exists
release
remove_clip_region
WEL_DC
require WEL_DC
exists: exists
round_rect (left, top, right, bottom, ellipse_width, ellipse_height: INTEGER_32)
`left'`top'
`right'`bottom'
`ellipse_width'`ellipse_height'
WEL_DC
require WEL_DC
exists: exists
save_bitmap (a_bitmap: WEL_BITMAP; file: FILE_NAME)
`a_bitmap'`file'
WEL_DC
require WEL_DC
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
file_not_void: file /= Void
file_is_valid: file.is_valid
select_clip_region (a_region: WEL_REGION)
`a_region'
WEL_DC
require WEL_DC
exists: exists
a_region_not_void: a_region /= Void
a_region_exists: a_region.exists
set_pixel (x, y: INTEGER_32; color: WEL_COLOR_REF)
`x'`y'
`color'
WEL_DC
require WEL_DC
exists: exists
color_not_void: color /= Void
stretch_blt (x_destination, y_destination, width_destination, height_destination: INTEGER_32; dc_source: WEL_DC; x_source, y_source, width_source, height_source, raster_operation: INTEGER_32)
`dc_source'
`x_source'
`y_source'`x_destination'`y_destination'
widthheight`raster_operation'
`raster_operation'
WEL_DC
require WEL_DC
exists: exists
positive_width_destination: width_destination >= 0
positive_height_destination: height_destination >= 0
positive_width_source: width_source >= 0
positive_height_source: height_source >= 0
dc_source_not_void: dc_source /= Void
dc_source_exists: dc_source.exists
stretch_di_bits (x_destination, y_destination, a_width, a_height, x_source, y_source, dib_width, dib_height: INTEGER_32; dib: WEL_DIB; bitmap_info: WEL_BITMAP_INFO; rgb_mode, raster_operation: INTEGER_32)
`x_source'`y_source'`x_destination'
`y_destination'`a_width'`a_height'
`raster_operation'`rgb_mode'
`raster_operation'
`rgb_mode'
WEL_DC
require WEL_DC
exists: exists
positive_width: a_width >= 0
positive_height: a_height >= 0
dib_not_void: dib /= Void
bitmap_not_void: bitmap_info /= Void
valid_rgb_mode: valid_dib_colors_constant (rgb_mode)
tabbed_text_out (x, y: INTEGER_32; string: STRING_GENERAL; tabulations: ARRAY [INTEGER_32]; tabulations_origin: INTEGER_32)
`string'`x'`y'
`tabulations'
`tabulations_origin'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
tabulations_not_void: tabulations /= Void
text_out (x, y: INTEGER_32; string: STRING_GENERAL)
`string'`x'`y'
WEL_DC
require WEL_DC
exists: exists
string_not_void: string /= Void
feature
io: STD_FILES
ANY
out: STRING_8
ANYtagged_out
ANY
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
feature
reference_tracked: BOOLEAN
`Current'
WEL_REFERENCE_TRACKABLE
references_count: INTEGER_32
WEL_REFERENCE_TRACKABLE
feature
decrement_reference
delete
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_references_started: reference_tracked
enable_reference_tracking
`references_tracked'
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_reference_not_started: not reference_tracked
increment_reference
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_references_started: reference_tracked
object_id: INTEGER_32
`Current'
WEL_REFERENCE_TRACKABLE
invariant
WEL_DC
valid_background_mode: exists implies is_opaque /= is_transparent
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
indexing
copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
source: "[
Eiffel Software
356 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Website http://www.eiffel.com
Customer support http://support.eiffel.com
]"
end WEL_SCREEN_DC