class interface PRINTER_DEVICE

creation
   make_default
      --  Create a printer device for the default printer, 
      --  if it exists.

      ensure
         can_fail:  --  is_ready = true or is_ready = false

feature(s) from MEMORY
   --  Removal :

   dispose
      --  Finalisation.


   full_collect
      --  Force a full collection cycle if garbage collection is
      --  enabled; do nothing otherwise.


feature(s) from GRAPHIC_DEVICE
   --  Access

   is_ready: BOOLEAN
      --  Is the device ready?


   prepare
      --  Get the device ready for graphic commands.

      require
         invalid: not is_ready
      ensure
         ready_at_creation: false;
         ready: is_ready

   release
      --  Invalidate graphic device.

      require
         ready: is_ready
      ensure
         invalid: not is_ready

feature(s) from GRAPHIC_DEVICE
   --  Capabilities

   capabilities: DEVICE_CAPABILITIES
      --  Device capabilities.


   text_capabilities: TEXT_METRICS
      --  Text capabilities.


feature(s) from GRAPHIC_DEVICE
   --  Coordinates conversions

   logical_to_device (pt: POINT): POINT
      --  Convert logical to device coordinates.

      require
         valid_point: pt /= Void;
         ready: is_ready
      ensure
         is_copy: Result /= Void

   device_to_logical (pt: POINT): POINT
      --  Convert device to logical coordinates.

      require
         valid_point: pt /= Void;
         ready: is_ready
      ensure
         is_copy: Result /= Void

feature(s) from GRAPHIC_DEVICE
   --  Set drawing attributes

   reset
      --  Reset attributes.


   set_mapping (mode: GRAPHIC_MAPPING)
      --  Set mapping mode.

      require
         valid_mode: mode /= Void

   set_mode (mode: GRAPHIC_MODE)
      --  Set the current graphic mode, used to determine how the 
      --  current pen and brush are applied. Note that it does not 
      --  apply to text.

      require
         valid_mode: mode /= Void;
         raster: capabilities.is_raster_display -- ?

   set_background_color (clr: COLOR)
      --  Set the current background color, used by the device 
      --  for text drawn with a background area, and to fill 
      --  gaps between some styled lines (using SIMPLE_PEN) 
      --  for instance.

      require
         valid: clr /= Void

   set_font (ft: FONT)
      --  Set current font.

      require
         valid_font: ft /= Void

   set_brush (br: BRUSH)
      --  Set current brush

      require
         valid_brush: br /= Void

   set_pen (pn: PEN)
      --  Set current pen.

      require
         valid_pen: pn /= Void

   set_palette (pal: PALETTE)
      --  Set current palette.

      require
         valid_pal: pal /= Void;
         possible: is_ready implies capabilities.has_palette; -- ? is_ready implies pal.size <= capabilities.palette_size
         good_size: 

feature(s) from GRAPHIC_DEVICE
   --  Clipping

   is_point_visible (pt: POINT): BOOLEAN
      --  Is point in the current clipping area?

      require
         valid_point: pt /= Void;
         ready: is_ready

   is_rectangle_visible (rect: RECTANGLE): BOOLEAN
      --  Does this rectangle has an intersection with the 
      --  current clipping area?

      require
         valid_rectangle: rect /= Void;
         ready: is_ready

feature(s) from GRAPHIC_DEVICE
   --  Actions

   draw (obj: DRAWABLE)
      --  Draw the drawable object.

      require
         valid_object: obj /= Void;
         ready: is_ready

feature(s) from GRAPHIC_DEVICE
   --  Text metrics

   text_extent (obj: DRAWABLE_TEXT): RECTANGLE
      --  Return the size of the bounding rectangle of the 
      --  text, as if it was drawn now.

      require
         valid_object: obj /= Void;
         ready: is_ready
      ensure
         is_copy: Result /= Void;
         origin: Result.lower.is_origin

   character_width (ch: CHARACTER): INTEGER
      --  Get witdh of a single character, as if it was drawn now.

      require
         ready: is_ready

feature(s) from GRAPHIC_DEVICE
   --  Colour 

   get_point_color (pt: POINT): COLOR
      --  Get pixel colour.

      require
         ready: is_ready;
         valid: pt /= Void;
         raster: capabilities.is_raster_display
      ensure
         void_if_outside:  --  color = Void if outside clipping rectangle

feature(s) from PRINTER_DEVICE
   --  Printing

   set_document_name (str: STRING)
      --  Document name for display in Print Manager.

      require
         valid: str /= Void

   start_document
      --  Start a document.


   end_document
      --  End the current document.


   start_page
      --  Start a page.


   end_page
      --  End the current page.


invariant
   valid_attrib: pen /= Void and brush /= Void and mapping /= Void;
   valid_caps: capabilities /= Void and then text_capabilities /= Void;
   valid_name: name /= Void;

end of PRINTER_DEVICE