expanded class interface BASIC_DIRECTORY
   --
   -- Very low-level basic tools for file-system directory handling and file
   -- path manipulation. This class is intended to be platform independant as
   -- much as possible. In order to remove from the client side the burden of
   -- file path computation, this class tries to compute automatically the
   -- system file notation using argument(s) of some of the very first call(s).
   -- As soon as the system notation has been properly detected, the result is
   -- internally memorized for all objects of type BASIC_DIRECTORY in a common
   -- private buffer. Besides the low-level nature of operations one can found
   -- in this class, all file path manipulations are done in a smart way
   -- (except when the system file path notation has not been detected
   -- automatically, which is quite uncommon). As an example, even if the
   -- directory separator is internally detected, this information is
   -- _intentionaly_ kept private to avoid low-level manipulation from the
   -- client side. Finally, this class is expanded in order to avoid as much as
   -- possible memory allocations.
   --
   -- Also consider high level facade class DIRECTORY if you don't want
   -- to deal directly with low level directory streams.
   --

feature(s) from BASIC_DIRECTORY
   -- State of Current basic directory stream:

   is_connected: BOOLEAN
      -- Is Current connected to some directory stream ?


   end_of_input: BOOLEAN
      -- Is end of input reached ?

      require
         is_connected

feature(s) from BASIC_DIRECTORY
   -- Connect and disconnect:

   connect_to (directory_path: STRING)
      -- Try to connect Current to some existing directory_path. After
      -- this call, the client is supposed to use is_connected to check
      -- that the stream is ready to be used.

      require
         not is_connected;
         not directory_path.is_empty;
         common_buffer_protection: last_entry /= directory_path
      ensure
         is_connected implies not end_of_input

   connect_with (some_path: STRING)
      -- Try to connect Current to some directory using some_path which
      -- may  be either an existing directory path or some arbitrary
      -- file path name. When some_path is the path of some readable
      -- existing directory, this directory is opened and the effect of
      -- connect_with is equivalent to connect_to. When some_path is not an
      -- existing readable directory path, connect_with tries to open the
      -- directory which may contains some_path viewed as a file path
      -- name. After this call, the client is supposed to use is_connected
      -- to check that the stream is ready to be used and the last_entry
      -- buffer to know about the corresponding opened directory path.
      -- Whatever the result, some_path is left unchanged.

      require
         not is_connected;
         not some_path.is_empty;
         common_buffer_protection: last_entry /= some_path
      ensure
         is_connected implies not end_of_input

   connect_to_current_working_directory
      -- Try to connect Current to the current working directory.
      -- After this call, the client is supposed to use is_connected
      -- to check that the stream is ready to be used and the last_entry
      -- buffer to know about the name of the current working directory.

      require
         not is_connected
      ensure
         is_connected implies not end_of_input

   disconnect
      -- Do not forget to call this feature when you have finished
      -- with some previously opened directory stream.

      require
         is_connected
      ensure
         not is_connected

feature(s) from BASIC_DIRECTORY
   -- Scanning:

   last_entry: STRING
      -- Unique global buffer (once object) to get the last information
      -- computed by many routines of this class: read_entry, connect_with
      -- connect_to_current_working_directory, compute_parent_directory_of, ...


   read_entry
      -- Read the next entry name and update last_entry and end_of_input
      -- accordingly.

      require
         is_connected;
         not end_of_input

feature(s) from BASIC_DIRECTORY
   -- File path handling tools:

   compute_parent_directory_of (some_path: STRING)
      -- Using some_path (which may be either a file path or a directory
      -- path) tries to compute in the last_entry buffer the parent
      -- directory of some_path. When some_path is a path with no parent
      -- directory, the last_entry buffer is_empty after this call. This
      -- operation does not perform any disk access.

      require
         not some_path.is_empty;
         common_buffer_protection: last_entry /= some_path

   compute_subdirectory_with (parent_path, entry_name: STRING)
      -- Try to compute in the last_entry buffer the new subdirectory
      -- path obtained when trying to concatenate smartly parent_path
      -- whith some entry_name. When this fails the last_entry buffer is_empty
      -- after this call. This operation does not perform any disk access.
      -- Whatever the result, parent_path and  entry_name are left unchanged.

      require
         not parent_path.is_empty;
         not entry_name.is_empty;
         common_buffer_protection1: last_entry /= parent_path;
         common_buffer_protection2: last_entry /= entry_name

   compute_file_path_with (parent_path, file_name: STRING)
      -- Try to compute in the last_entry buffer the new file path obtained
      -- when trying to concatenate smartly parent_path whith some
      -- file_name. When this fails the last_entry buffer is_empty after
      -- this call. This operation does not perform any disk access.
      -- Whatever the result, parent_path and file_name are left unchanged.

      require
         not parent_path.is_empty;
         not file_name.is_empty;
         common_buffer_protection1: last_entry /= parent_path;
         common_buffer_protection2: last_entry /= file_name

   change_current_working_directory (directory_path: STRING)
      -- Try to change the current working directory using some
      -- directory_path. When the operation is possible, the last_entry buffer
      -- is updated with the new current working directory path,
      -- otherwise, when the modification is not possible the last_entry
      -- buffer is_empty after this call. Whatever the result,
      -- directory_path is left unchanged.

      require
         not is_connected;
         common_buffer_protection1: last_entry /= directory_path
      ensure
         not is_connected

feature(s) from BASIC_DIRECTORY
   -- Disk modification:

   create_new_directory (directory_path: STRING): BOOLEAN
      -- Try to create a new directory using the directory_path name.
      -- Returns true on success.

      require
         not is_connected
      ensure
         not is_connected

   remove_directory (directory_path: STRING): BOOLEAN
      -- Try to remove directory directory_path which must be empty.
      -- Returns true on success.

      require
         not is_connected
      ensure
         not is_connected

   remove_files_of (directory_path: STRING)
      -- Try to remove all files (not subdirectories) of directory
      -- specified by directory_path.

      require
         not is_connected
      ensure
         not is_connected

feature(s) from BASIC_DIRECTORY
   -- Miscellaneous:

   is_case_sensitive: BOOLEAN



end of expanded BASIC_DIRECTORY