indexing
description: "Representation of a typeface.Appearance is specified in terms of font family, height, shape andweight. The local system font closest to the specification will bedisplayed. A specific font name may optionally be specified. See `set_preferred_face'"
status: "See notice at end of class"
keywords: "character, face, height, family, weight, shape, bold, italic"
date: "$Date$"
revision: "$Revision$"
class interface
EV_FONT
create
frozen default_create
EV_ANY
ensure then EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state
make_with_values (a_family, a_weight, a_shape, a_height: INTEGER)
a_familya_weighta_shapea_height
require
a_family_valid: valid_family (a_family)
a_weight_valid: valid_weight (a_weight)
a_shape_valid: valid_shape (a_shape)
a_height_bigger_than_zero: a_height > 0
ensure
a_family_set: family = a_family
a_weight_set: weight = a_weight
a_shape_set: shape = a_shape
a_height_set: height = a_height
feature
data: ANY
EV_ANY
family: INTEGER
EV_FONT_CONSTANTS
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.family
height: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.height
preferred_families: ACTIVE_LIST [STRING]
family
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.preferred_families
result_not_void: Result /= void
shape: INTEGER
EV_FONT_CONSTANTS
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.shape
weight: INTEGER
EV_FONT_CONSTANTS
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.weight
feature
ascent: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.ascent
descent: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.descent
horizontal_resolution: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.horizontal_resolution
is_proportional: BOOLEAN
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.is_proportional
maximum_width: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.maximum_width
minimum_width: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.minimum_width
name: STRING
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result.is_equal (implementation.name)
string_size (a_string: STRING): TUPLE [INTEGER, INTEGER]
a_string
require
not_destroyed: not is_destroyed
a_string_not_void: a_string /= void
ensure
bridge_ok: Result.item (1).is_equal (implementation.string_size (a_string).item (1)) and Result.item (2).is_equal (implementation.string_size (a_string).item (2))
string_width (a_string: STRING): INTEGER
a_string
require
not_destroyed: not is_destroyed
a_string_not_void: a_string /= void
ensure
bridge_ok: Result = implementation.string_width (a_string)
positive: Result >= 0
vertical_resolution: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.vertical_resolution
width: INTEGER
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.width
feature
set_data (some_data: like data)
some_datadata
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
set_family (a_family: INTEGER)
a_familyfamily
require
not_destroyed: not is_destroyed
a_family_valid: valid_family (a_family)
ensure
family_assigned: family = a_family
set_height (a_height: INTEGER)
a_heightheight
require
not_destroyed: not is_destroyed
a_height_bigger_than_zero: a_height > 0
ensure
height_assigned: height = a_height
set_shape (a_shape: INTEGER)
a_shapeshape
require
not_destroyed: not is_destroyed
a_shape_valid: valid_shape (a_shape)
ensure
shape_assigned: shape = a_shape
set_weight (a_weight: INTEGER)
a_weightweight
require
not_destroyed: not is_destroyed
a_weight_valid: valid_weight (a_weight)
ensure
weight_assigned: weight = a_weight
feature
copy (other: like Current)
Currentother
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
is_equal (other: like Current): BOOLEAN
other
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
valid_family (a_family: INTEGER): BOOLEAN
a_family
EV_FONT_CONSTANTS
valid_shape (a_shape: INTEGER): BOOLEAN
a_shape
EV_FONT_CONSTANTS
valid_weight (a_weight: INTEGER): BOOLEAN
a_weight
EV_FONT_CONSTANTS
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
family_valid: is_initialized implies valid_family (family)
weight_valid: is_initialized implies valid_weight (weight)
shape_valid: is_initialized implies valid_shape (shape)
height_bigger_than_zero: is_initialized implies height > 0
ascent_bigger_than_zero: is_initialized implies ascent > 0
descent_bigger_than_zero: is_initialized implies descent > 0
height_positive: is_initialized implies height > 0
ascent_positive: is_initialized implies ascent > 0
descent_positive: is_initialized implies descent > 0
width_of_empty_string_equals_zero: is_initialized implies string_width ("") = 0
horizontal_resolution_non_negative: is_initialized implies horizontal_resolution >= 0
vertical_resolution_non_negative: is_initialized implies vertical_resolution >= 0
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
end -- EV_FONT