deferred class interface ES_MULTIPLEXED_SOCKET_WRITER
   -- 
   --  An abstraction for a socket whose output is managed through a multiplexer.
   -- 

feature(s) from ES_MULTIPLEXER_SINGLETON
   --  The Multiplexer

   multiplexer: ES_STANDALONE_MULTIPLEXER_POLL
      --  The Multiplexer
      ensure
         not_void: Result /= Void

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Accessors

   id: INTEGER
      --  Unique integer that identifies this device

   open: BOOLEAN
      --  Is the underlying I/O device open?

   closed: BOOLEAN
      --  Is the underlying I/O device closed?

   in_multiplexer: BOOLEAN
      --  Is this object in the multiplexer?
      ensure
         definition: Result = multiplexer.has(Current)

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Multiplexer State Control

   put_in_multiplexer
      --  Put Current into the multiplexer.
      require
         not_yet_in_multiplexer: not in_multiplexer
      ensure
         in_multiplexer: in_multiplexer

   remove_from_multiplexer
      --  Remove Current from the multiplexer.
      require
         in_multiplexer: in_multiplexer
      ensure
         not_in_multiplexer: not in_multiplexer

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Cleanup

   clean_up
      --  Clean up the resources of this device.
      require
         now_open: open
      ensure
         not_in_multiplexer: not in_multiplexer;
         closed: closed

feature(s) from ES_MULTIPLEXED_SOCKET_WRITER
   --  Accessors

   managed_socket: ES_STREAM_SOCKET
      --  The socket that this stream manages

   is_set_to_write: BOOLEAN
      --  Is this object set to send data?
      ensure
         Result = (in_multiplexer and then multiplexer.device_flagged_for_output(Current))

   data_present: BOOLEAN
      --  Is there data set to be sent?

feature(s) from ES_MULTIPLEXED_SOCKET_WRITER
   --  I/O Helpers

   set_to_write (mode: BOOLEAN)
      --  Sets this object to multiplex writing according to mode.
      require
         in_multiplexer: in_multiplexer;
         write_buffer_present: mode implies data_present
      ensure
         set: is_set_to_write = mode

   safely_put (text: STRING)
      --  Writes text in a manner ensured not to block. Will
      --  buffer data if needed and control the multiplexer.
      require
         not_void: text /= Void;
         not_empty: not text.empty
      ensure
         maybe_buffered: data_present or not data_present;
         buffering_automatic: data_present = is_set_to_write

   add_to_buffer (text: STRING)
      --  Add text to the output buffer.
      require
         not_void: text /= Void;
         not_empty: not text.empty
      ensure
         data_present: data_present

   new_buffer (text: STRING)
      --  Make text the new buffer for output. text is aliased.
      require
         no_other_data_to_lose: not data_present;
         not_void: text /= Void;
         not_empty: not text.empty
      ensure
         data_present: data_present

   clean_up_when_ready
      --  Clean up just when all buffers are nicely flushed.

   send_end_of_data_when_ready
      --  Send an end_of_data indicator after buffers are nicely
      --  flushed.

feature(s) from ES_MULTIPLEXED_SOCKET_WRITER
   --  Callback

   refill_write_buffer
      --  The write buffer has been flushed; refill it if needed. 
      --  (Default: nothing)

   error_notification
      --  An error occured.

invariant

    in_multiplexer: in_multiplexer implies open;

    closed_is_not_open: closed = not open;

    managed_socket_not_void: managed_socket /= Void;

end of deferred ES_MULTIPLEXED_SOCKET_WRITER