class interface PAGE_MAPPING
creation
make
feature(s) from PAGE_MAPPING
-- General
copy (other: like Current)
-- Update current object using fields of object attached
-- to other, so as to yield equal objects.
require
other_not_void: other /= Void
ensure
is_equal: is_equal(other)
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered equal to
-- current object ?
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
feature(s) from PAGE_MAPPING
-- Modes
is_cartesian: BOOLEAN
-- Is the current mapping mode cartesian?
-- Cartesian means x coordinates grow rightward, y when
-- downwards, and that circles are round and squares square
-- (the device is isotropic).
text
-- Pixel (device) coordinates; x to the right, y downwards
low_metric
-- 0.1 millimetre, cartesian.
high_metric
-- 0.01 millimetre, cartesian.
low_english
-- 0.01 inch, cartesian.
high_english
-- 0.001 inch, cartesian.
twip
-- 1/20th of a point (1/1440th of an inch), cartesian.
feature(s) from PAGE_MAPPING
-- Origin
set_origin (pt: POINT)
-- Set where the physical device origin (0, 0) is relatively to
-- the new logical origin of the device (in logical coordinates).
require
valid_point: pt /= Void
end of PAGE_MAPPING