indexing
description: "General notion of a device context."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2007-08-23 14:55:50 -0700 (Thu, 23 Aug 2007) $"
revision: "$Revision: 70106 $"
deferred class interface
WEL_DC
feature
bitmap: WEL_BITMAP
brush: WEL_BRUSH
font: WEL_FONT
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
item: POINTER
WEL_ANY
palette: WEL_PALETTE
pen: WEL_PEN
region: WEL_REGION
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 (other /= Void and then 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))
frozen is_deep_equal (other: WEL_DC): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure 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: WEL_DC): 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: WEL_DC): 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
require
exists: exists
ensure
result_not_void: Result /= Void
bitmap_selected: BOOLEAN
brush_selected: BOOLEAN
char_abc_widths (first_char_index, last_char_index: NATURAL_32): ARRAYED_LIST [WEL_ABC_STRUCT]
`Result'
`first_char_index'`last_char_index'
require
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
result_not_void: Result /= Void
character_size (c: CHARACTER_8): WEL_SIZE
`s'
require
exists: exists
ensure
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'
require
exists: exists
exists: BOOLEAN
item
WEL_ANY
require WEL_REFERENCE_TRACKABLE
True
ensure WEL_ANY
Result = (item /= default_pointer)
font_selected: BOOLEAN
height: INTEGER_32
require
exists: exists
is_opaque: BOOLEAN
require
exists: exists
is_transparent: BOOLEAN
require
exists: exists
map_mode: INTEGER_32
require
exists: exists
ensure
valid_map_mode: valid_map_mode_constant (Result)
mask_blt_supported: BOOLEAN is True
palette_selected: BOOLEAN
pen_selected: BOOLEAN
pixel_color (x, y: INTEGER_32): WEL_COLOR_REF
`x'`y'
require
exists: exists
ensure
result_not_void: Result /= Void
polygon_fill_mode: INTEGER_32
require
exists: exists
ensure
valid_polygon_fill_mode: valid_polygon_fill_mode_constant (Result)
position: WEL_POINT
require
exists: exists
ensure
result_exists: Result /= Void
region_selected: BOOLEAN
rop2: INTEGER_32
require
exists: exists
ensure
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
require
exists: exists
ensure
valid_stretch_mode: valid_stretch_mode_constant (Result)
string_height (s: STRING_GENERAL): INTEGER_32
`s'
require
exists: exists
s_exists: s /= Void
ensure
positive_result: Result >= 0
string_size (s: STRING_GENERAL): WEL_SIZE
`s'
require
exists: exists
s_exists: s /= Void
ensure
result_exists: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
string_width (s: STRING_GENERAL): INTEGER_32
`s'
require
exists: exists
s_exists: s /= Void
ensure
positive_result: Result >= 0
tabbed_text_height (text: STRING_GENERAL): INTEGER_32
`text'
require
exists: exists
text_not_void: text /= Void
ensure
positive_height: Result >= 0
tabbed_text_size (text: STRING_GENERAL): WEL_SIZE
`text'
require
exists: exists
text_not_void: text /= Void
ensure
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'
require
exists: exists
text_not_void: text /= Void
tabulations_not_void: tabulations /= Void
ensure
result_not_void: Result /= Void
positive_width: Result.width >= 0
positive_height: Result.height >= 0
tabbed_text_width (text: STRING_GENERAL): INTEGER_32
`text'
require
exists: exists
text_not_void: text /= Void
ensure
positive_width: Result >= 0
text_alignment: INTEGER_32
require
exists: exists
text_color: WEL_COLOR_REF
require
exists: exists
ensure
result_not_void: Result /= Void
text_face: STRING_GENERAL
require
exists: exists
ensure
result_not_void: Result /= Void
valid_dib_colors_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_DIB_COLORS_CONSTANTS
valid_extent_map_mode (mode: INTEGER_32): BOOLEAN
`mode'
require
valid_map_mode: valid_map_mode_constant (mode)
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
viewport_extent: WEL_SIZE
require
exists: exists
ensure
result_not_void: Result /= Void
viewport_origin: WEL_POINT
require
exists: exists
ensure
result_not_void: Result /= Void
width: INTEGER_32
require
exists: exists
window_extent: WEL_SIZE
require
exists: exists
ensure
result_not_void: Result /= Void
window_origin: WEL_POINT
require
exists: exists
ensure
result_not_void: Result /= Void
feature
select_bitmap (a_bitmap: WEL_BITMAP)
`a_bitmap'
require
exists: exists
a_bitmap_not_void: a_bitmap /= Void
a_bitmap_exists: a_bitmap.exists
ensure
bitmap_set: bitmap = a_bitmap
bitmap_selected: bitmap_selected
select_brush (a_brush: WEL_BRUSH)
`a_brush'
require
exists: exists
a_brush_not_void: a_brush /= Void
a_brush_exists: a_brush.exists
ensure
brush_set: brush = a_brush
brush_selected: brush_selected
select_font (a_font: WEL_FONT)
`a_font'
require
exists: exists
a_font_not_void: a_font /= Void
a_font_exists: a_font.exists
ensure
font_set: font = a_font
font_selected: font_selected
select_palette (a_palette: WEL_PALETTE)
`a_palette'
require
exists: exists
a_palette_not_void: a_palette /= Void
a_palette_exists: a_palette.exists
select_pen (a_pen: WEL_PEN)
`a_pen'
require
exists: exists
a_pen_not_void: a_pen /= Void
a_pen_exists: a_pen.exists
ensure
pen_set: pen = a_pen
pen_selected: pen_selected
select_region (a_region: WEL_REGION)
`a_region'
require
exists: exists
a_region_not_void: a_region /= Void
a_region_exists: a_region.exists
ensure
region_set: region = a_region
region_selected: region_selected
set_background_color (color: WEL_COLOR_REF)
background_color`color'
require
exists: exists
color_not_void: color /= Void
ensure
color_set: background_color.item = color.item
set_background_opaque
require
exists: exists
ensure
is_opaque: is_opaque
set_background_transparent
require
exists: exists
ensure
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'
require
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'
require
exists: exists
valid_horizontal_alignment: valid_htext_alignment_constant (h)
valid_vertical_alignment: valid_vtext_alignment_constant (v)
ensure
text_alignments_set: flag_set (text_alignment, h) and flag_set (text_alignment, v)
set_map_mode (mode: INTEGER_32)
`mode'
`mode'
require
exists: exists
valid_map_mode: valid_map_mode_constant (mode)
ensure
map_mode_set: map_mode = mode
set_polygon_fill_mode (mode: INTEGER_32)
polygon_fill_mode
`mode'
`mode'
require
exists: exists
valid_polygon_fill_mode: valid_polygon_fill_mode_constant (mode)
ensure
polygon_fill_mode_set: polygon_fill_mode = mode
set_rop2 (a_rop2: INTEGER_32)
`a_rop2'
require
exists: exists
valid_rop2_constant: valid_rop2_constant (a_rop2)
ensure
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'
require
exists: exists
valid_stretch_mode_constant: valid_stretch_mode_constant (a_mode)
ensure
stretch_blt_mode_set: stretch_blt_mode = a_mode
set_text_alignment (an_alignment: INTEGER_32)
`an_alignment'
`an_alignment'
require
exists: exists
valid_alignment: valid_text_alignment_constant (an_alignment)
ensure
text_alignment_set: flag_set (text_alignment, an_alignment)
set_text_color (color: WEL_COLOR_REF)
text_color`color'
require
exists: exists
color_not_void: color /= Void
ensure
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'
require
exists: exists
valid_current_map_mode: valid_extent_map_mode (map_mode)
ensure
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'
require
exists: exists
ensure
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'
require
exists: exists
valid_current_map_mode: valid_extent_map_mode (map_mode)
ensure
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'
require
exists: exists
ensure
x_window_origin_set: window_origin.x = x_origin
y_window_origin_set: window_origin.y = y_origin
unselect_all
require
exists: exists
ensure
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
require
exists: exists
bitmap_selected: bitmap_selected
ensure
bitmap_not_selected: not bitmap_selected
unselect_brush
require
exists: exists
brush_selected: brush_selected
ensure
brush_not_selected: not brush_selected
unselect_font
require
exists: exists
font_selected: font_selected
ensure
font_not_selected: not font_selected
unselect_palette
require
exists: exists
palette_selected: palette_selected
ensure
palette_not_selected: not palette_selected
unselect_pen
require
exists: exists
pen_selected: pen_selected
ensure
pen_not_selected: not pen_selected
unselect_region
require
exists: exists
region_selected: region_selected
ensure
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: WEL_DC)
`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: WEL_DC)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: WEL_DC
ANY
ensure ANY
deep_twin_not_void: Result /= Void
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: WEL_DC)
`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: WEL_DC
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: WEL_DC
`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: <