class interface DIRECTORY
   --
   -- Tools for file-system directory handling.
   -- High-level facade for class BASIC_DIRECTORY.
   --

creation
   make
      -- Make a new not assigned one.

      ensure
         is_empty

   scan (directory_path: STRING)
      -- Try to scan some existing directory_path which is supposed to be a 
      -- correctly spelled directory path. After this call the client is 
      -- supposed to check last_scan_status to know. So, when last_scan_status is 
      -- true after this call, the entire directory has been read.

      require
         not directory_path.is_empty
      ensure
         not last_scan_status implies is_empty

   scan_with (some_path: STRING)
      -- Try to scan Current using some_path where some_path can be
      -- either a file path or an existing directory path.
      -- When some_path is a directory path, the behavior is equivalent
      -- to connect_to.
      -- When some_path is the path of an existing file, the directory
      -- which contains this file is scanned.

      require
         not some_path.is_empty
      ensure
         not last_scan_status implies is_empty

   scan_current_working_directory
      ensure
         not last_scan_status implies is_empty

feature(s) from DIRECTORY   path: STRING
      -- The directory path in use (see scan).


   last_scan_status: BOOLEAN
      -- True when last scan (or last re_scan) has sucessfully
      -- read some existing directory using path.


feature(s) from DIRECTORY
   -- Disk access:

   scan (directory_path: STRING)
      -- Try to scan some existing directory_path which is supposed to be a 
      -- correctly spelled directory path. After this call the client is 
      -- supposed to check last_scan_status to know. So, when last_scan_status is 
      -- true after this call, the entire directory has been read.

      require
         not directory_path.is_empty
      ensure
         not last_scan_status implies is_empty

   scan_with (some_path: STRING)
      -- Try to scan Current using some_path where some_path can be
      -- either a file path or an existing directory path.
      -- When some_path is a directory path, the behavior is equivalent
      -- to connect_to.
      -- When some_path is the path of an existing file, the directory
      -- which contains this file is scanned.

      require
         not some_path.is_empty
      ensure
         not last_scan_status implies is_empty

   scan_subdirectory (subdirectory: STRING)
      -- Try to scan the given subdirectory of the current one. "." and
      -- ".." are not scanned.

      require
         has(subdirectory)

   scan_parent_directory
      -- Try to scan the parent directory, if it exists. If notm the
      -- directory is unchanged.


   re_scan
      -- Update internal information by reloading all the information
      -- about the path directory from the disk.
      -- Update last_scan_status, count, and all items.

      require
         path /= Void
      ensure
         not last_scan_status implies is_empty

   scan_current_working_directory
      ensure
         not last_scan_status implies is_empty

feature(s) from DIRECTORY
   -- Access:

   lower: INTEGER
      -- Index of the first item.


   upper: INTEGER
      -- Index of the last item.


   count: INTEGER
      -- Number of items (files or directories) in Current.

      ensure
         Result >= 0

   is_empty: BOOLEAN
      ensure
         definition: Result = (count = 0)

   valid_index (index: INTEGER): BOOLEAN
      ensure
         Result = (lower <= index and index <= upper)

   item (index: INTEGER): STRING
      -- Return the name of entry (file or subdirectory) at index.

      require
         valid_index(index)
      ensure
         has(Result)

   name (index: INTEGER): STRING
      -- Return the name of entry (file or subdirectory) at index.

      require
         valid_index(index)
      ensure
         has(Result)

   has (entry_name: STRING): BOOLEAN
      -- Does Current contain the entry_name (file or subdirectory) ?

      require
         not entry_name.is_empty

feature(s) from DIRECTORY
   -- File access:

   connect_to_file (file: FILE; filename: STRING)
      -- Connect the file to the operating system file given by its
      -- filename, which must be a file of the current directory.

      require
         file /= Void;
         has(filename)
      ensure
         file.is_connected



end of DIRECTORY