class interface DEVICE_CAPABILITIES

feature(s) from DEVICE_CAPABILITIES
   --  Precondition

   is_device_ready: BOOLEAN
      --  Is the parent device valid?


feature(s) from DEVICE_CAPABILITIES
   --  Device type

   is_plotter: BOOLEAN
      --  Is the device a plotter?

      require
         ready: is_device_ready

   is_raster_display: BOOLEAN
      --  Is the device a raster display?

      require
         ready: is_device_ready

   is_raster_printer: BOOLEAN
      --  Is the device a raster printer?

      require
         ready: is_device_ready

   is_raster_camera: BOOLEAN
      --  Is the device a raster camera?

      require
         ready: is_device_ready

   is_character_stream: BOOLEAN
      --  Is the device a character stream?

      require
         ready: is_device_ready

   is_metafile: BOOLEAN
      --  Is the device a metafile?

      require
         ready: is_device_ready

   is_display_file: BOOLEAN
      --  Is the device a display file?

      require
         ready: is_device_ready

feature(s) from DEVICE_CAPABILITIES
   --  Device size and definition

   width_mm: INTEGER
      --  Width of the device screen (millimetres).

      require
         ready: is_device_ready

   height_mm: INTEGER
      --  Height of the device screen (millimetres).

      require
         ready: is_device_ready

   width_pixel: INTEGER
      --  Width of the device screen (pixels).

      require
         ready: is_device_ready

   height_pixel: INTEGER
      --  Height of the device screen (pixels).

      require
         ready: is_device_ready

   width_dpi: INTEGER
      --  Number of pixel per inch (dot-per-inch) along the horizontal axis.

      require
         ready: is_device_ready

   height_dpi: INTEGER
      --  Number of pixel per inch (dot-per-inch) along the vertical axis.

      require
         ready: is_device_ready

   screen_pixel: RECTANGLE
      --  Helper function providing rectangle of screen in pixels for 
      --  window positioning, etc.

      require
         ready: is_device_ready
      ensure
         is_copy: Result /= Void

feature(s) from DEVICE_CAPABILITIES
   --  Colors

   color_bits_per_pixel: INTEGER
      --  Number of adjacent colour bits for each pixel.

      require
         ready: is_device_ready

   color_plane: INTEGER
      --  Number of colour planes.

      require
         ready: is_device_ready

   color_number: INTEGER
      --  Number of colours currently available (typically 20 on screens).

      require
         ready: is_device_ready

   has_palette: BOOLEAN
      --  Is display palettised (or true colour)?

      require
         ready: is_device_ready

   palette_bits_per_pixel: INTEGER
      --  Actual colour resolution of a palettised device in bits per pixel.

      require
         ready: is_device_ready;
         palette: has_palette

   palette_reserved: INTEGER
      --  Number of reserved entries in the system palette.

      require
         ready: is_device_ready;
         palette: has_palette

   palette_size: INTEGER
      --  Nymber of entries in the system palette.

      require
         ready: is_device_ready;
         palette: has_palette

feature(s) from DEVICE_CAPABILITIES
   --  Raster capabilities

   has_raster_bitmap: BOOLEAN
      --  Has raster capabilities? (pixel, bitmap transfer)

      require
         ready: is_device_ready

feature(s) from DEVICE_CAPABILITIES
   --  Text capabilities

   can_rotate_text: BOOLEAN
      --  Can the device rotate text?

      require
         ready: is_device_ready

   can_rotate_text_90: BOOLEAN
      --  Can the device rotate text at 90, 180, 270 degrees?

      require
         ready: is_device_ready
      ensure
         implication: can_rotate_text

invariant
   device_exist: parent /= Void;

end of DEVICE_CAPABILITIES