deferred class interface ES_MULTIPLEXED_SOCKET_READER
   -- 
   --  An object that both sends and receives data 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_READER
   --  Accessors

   managed_socket: ES_STREAM_SOCKET
      --  The socket managed by Current

   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

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

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_READER