deferred class interface ES_MULTIPLEXED_CONSOLE
   -- 
   --  A multiplexed device that will respond asychonously to console
   --  input. Console output is managed by this class, but is delivered
   --  by the normal Eiffel Kernel classes.
   -- 

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

   open: BOOLEAN
      --  Is the 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 ES_MULTIPLEXED_CONSOLE
   --  Accessors

   is_set_to_read: BOOLEAN
      --  Is this device set to read from the console?

feature(s) from ES_MULTIPLEXED_CONSOLE
   --  Modifiers

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

feature(s) from ES_MULTIPLEXED_CONSOLE
   --  Callbacks

   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;

end of deferred ES_MULTIPLEXED_CONSOLE