deferred class interface FILE
   --
   -- Common parent class to all the FILE-type streams. Provides a common
   -- connection interface to the "real" files of the operating system.
   --

feature(s) from FILE   is_connected: BOOLEAN
      -- Is this file connected to some file of the operating system?


   connect_to (new_path: STRING)
      -- Try to connect to an existing file of the operating system.

      require
         not is_connected;
         not new_path.is_empty

   disconnect
      -- Disconnect from any file.

      require
         is_connected
      ensure
         not is_connected



end of deferred FILE