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