deferred class interface ES_MULTIPLEXED_SOCKET
   -- 
   --  An abstraction of a socket whose reading and writing are 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 identifier for this socket
      ensure
         definition: Result = managed_socket.id

   open: BOOLEAN
      --  Is the socket open?
      ensure
         definition: Result = managed_socket.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
      --  Close the device, clean up resources, and free the multiplexer
      --  connection.
      require
         now_open: open
      ensure
         buffer_empty: not data_present;
         not_in_multiplexer: not in_multiplexer;
         closed: closed

feature(s) from ES_MULTIPLEXED_SOCKET_READER
   --  Accessors

   managed_socket: ES_STREAM_SOCKET
      --  The socket that this stream manages

   is_set_to_read: BOOLEAN
      --  Is this object set to receive data?
      ensure
         definition: Result = (in_multiplexer and then multiplexer.device_flagged_for_input(Current))

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

   set_to_read (mode: BOOLEAN)
      --  Sets this object to recieve input according to mode.
      require
         in_multiplexer: in_multiplexer
      ensure
         set: is_set_to_read = mode

feature(s) from ES_MULTIPLEXED_SOCKET_READER
   --  Callback Notifications

   data_ready (text: STRING)
      --  The data text has been read and must be processed.
      require
         in_multiplexer: in_multiplexer;
         not_void: text /= Void;
         set_to_read: is_set_to_read

   end_of_data
      --  An end of data has been reached.
      require
         in_multiplexer: in_multiplexer;
         will_read_no_more: not is_set_to_read
      ensure
         read_no_more: not is_set_to_read

   read_error_notification
      --  Called when an error occurs on I/O.

feature(s) from ES_MULTIPLEXED_SOCKET_WRITER
   --  Accessors

   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)

   write_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;

    managed_socket_not_void: managed_socket /= Void;

end of deferred ES_MULTIPLEXED_SOCKET