deferred class interface ES_MULTIPLEXED_SERVER_SOCKET
   -- 
   --  An ES_MULTIPLEXED_DEVICE that implements management for an
   --  ES_SERVER_SOCKET.
   -- 

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 the 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
         not_in_multiplexer: not in_multiplexer;
         closed: closed

feature(s) from KL_SHARED_EXCEPTIONS
   --  Access

   exceptions: KL_EXCEPTIONS
      --  Exception handling
      ensure
         exceptions_not_void: Result /= Void

feature(s) from ES_MULTIPLEXED_SERVER_SOCKET
   --  Accessors

   managed_socket: ES_SERVER_SOCKET
      --  The socket that Current manages

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

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

   set_to_receive_connections (mode: BOOLEAN)
      --  Sets this object to recieve connections according to mode.
      require
         in_multiplexer: in_multiplexer
      ensure
         set: is_set_to_receive_connections = mode

feature(s) from ES_MULTIPLEXED_SERVER_SOCKET
   --  Callback Notifications

   new_connection (socket: ES_STREAM_SOCKET)
      --  The new connection socket has arrived and must be
      --  handled.
      require
         in_multiplexer: in_multiplexer;
         set_to_read: is_set_to_receive_connections;
         good_socket: not socket.error and socket.connected

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

invariant

    in_multiplexer: in_multiplexer implies open;

    closed_is_not_open: closed = not open;

    socket_present: managed_socket /= Void;

    socket_non_blocking: managed_socket.non_blocking;

end of deferred ES_MULTIPLEXED_SERVER_SOCKET