indexing
description: "Memory device context compatible with a given 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_COMPATIBLE_DC
create
make (a_dc: WEL_DC)
`a_dc'
require
a_dc_not: a_dc /= Void
a_dc_exists: a_dc.exists
ensure
exists: exists
feature
bitmap: WEL_BITMAP
WEL_DC
brush: WEL_BRUSH
WEL_DC
font: WEL_FONT
WEL_DC
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
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 (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_COMPATIBLE_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_COMPATIBLE_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_COMPATIBLE_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
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 is True
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_dib_colors_constant (c: INTEGER_32): BOOLEAN
`c'
WEL_DIB_COLORS_CONSTANTS
valid_extent_map_mode (mode: INTEGER_32): BOOLEAN
`mode'
WEL_DC
require WEL_DC
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
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
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