class interface METAFILE_DEVICE

creation
   make_file (refdev: GRAPHIC_DEVICE; width, height: INTEGER; file: STRING)
      --  Create (enhanced) metafile named file, from 
      --  exisiting device, fitting in a rectangle of 
      --  width and height (0.01 mm units).

      require
         valid_reference: refdev /= Void and then refdev.is_ready;
         valid_size: width > 0 and height > 0;
         valid_file: file /= Void
      ensure
         done:  --  is_ready if success.

   make_memory (refdev: WINDOW_DEVICE; width, height: INTEGER)
      --  Create a memory metafile.

      require
         valid_reference: refdev /= Void and then refdev.is_ready;
         valid_size: width > 0 and height > 0
      ensure
         done:  --  is_ready if success.

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
      --  Device is ready at creation.

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

   release
      --  Release the device (close metafile).

      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

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

end of METAFILE_DEVICE