class interface BASIC_DIRECTORY
   -- 
   --  Low-level basic tools for file-system directory handling.
   -- 
   --  Also consider hight level facade class DIRECTORY for a safer usage.
   -- 

creation
   make
      --  Make a new object which is _not_ connected to any 
      --  directory on disk.
      --  Use set_path to connect Current to a directory on disk.


feature(s) from BASIC_DIRECTORY
   path: STRING
      --  Void or some path which may be absolute or not (see set_path).


   name_list: FIXED_ARRAY[STRING]
      --  Actual list of entries (files or subdirectories)..


feature(s) from BASIC_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

   valid_index (index: INTEGER): BOOLEAN
      ensure
         Result = index.in_range(0,upper)

   is_subdirectory (index: INTEGER): BOOLEAN
      --  Is the item at index a subdirectory ?

      require
         valid_index(index)

   is_file (index: INTEGER): BOOLEAN
      --  Is the item at index a file ?

      require
         valid_index(index)
      ensure
         Result = not is_subdirectory(index)

   absolute_path: STRING
      --  Gives acces to the absolute path of Current.

      ensure
         Result /= Void

   absolute_path_of (index: INTEGER): STRING
      --  Gives access to absolute path of item at index.

      require
         valid_index(index)
      ensure
         Result /= Void

   get_parent_directory: like Current
      --  Get new object corresponding to parent directory.
      --  Return Void in case of failure.
      --  Also consider go_parent_directory.


   get_subdirectory (index: INTEGER): like Current
      --  Get new directory object corresponding to item at index.
      --  Return Void in case of failure.
      --  Also consider go_subdirectory.

      require
         is_subdirectory(index)

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

      require
         not entry_name.empty

   index_of (entry_name: STRING): INTEGER
      --  Index of entry_name (file or subdirectory).
      --  Return count + 1 if not found.

      ensure
         Result = count + 1 or valid_index(Result)

   has_file (filename: STRING): BOOLEAN
      --  Does Current contain filename as an entry for a file ?

      require
         not filename.empty
      ensure
         Result implies is_file(index_of(filename))

   has_subdirectory (dirname: STRING): BOOLEAN
      --  Does Current contain dirname as an entry for a subdirectory ?

      require
         not dirname.empty
      ensure
         Result implies is_subdirectory(index_of(dirname))

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

      require
         valid_index(index)
      ensure
         has(Result)

feature(s) from BASIC_DIRECTORY
   --  Modification :

   go_parent_directory: BOOLEAN
      --  Change Current to its parent directory; do not change 
      --  anything in case of failure.
      --  Return true if succeeded, false otherwise.
      --  Also consider get_parent_directory.


   go_subdirectory (index: INTEGER): BOOLEAN
      --  Change Current to subdirectory at index; do not change 
      --  anything in case of failure.
      --  Return true if succeeded, false otherwise.
      --  Also consider get_subdirectory.

      require
         is_subdirectory(index)

feature(s) from BASIC_DIRECTORY
   --  Disk access :

   update: BOOLEAN
      --  Update Current status by reloading information from the 
      --  disk.
      --  Return true if succeeded, false otherwise.


feature(s) from BASIC_DIRECTORY
   --  Disk access :

   set_path (p: like path): BOOLEAN
      --  Connects Current to the existing directory path on disk.
      --  Support of absolute and/or relative paths is not guaranteed for 
      --  portability reasons. :-)
      --  Return true if succeeded, false otherwise.
      --  In case of success, update has been successfully done.

      require
         not p.empty
      ensure
         Result implies path = p

feature(s) from BASIC_DIRECTORY
   --  current directory handling :

   current_working_directory
      --  Update Current with the current working directory.


feature(s) from BASIC_DIRECTORY
   --  Disk modification :

   create_subdirectory (dirname: STRING): BOOLEAN
      --  Create a new (one-level) subdirectory dirname on disk.
      --  Nested creations support and semantics are not guaranteed for 
      --  portability reasons.
      --  Return true if succeeded, false otherwise.
      --  In case of success, update has been successfully done.

      require
         not has(dirname)

   delete_subdirectory (dirname: STRING): BOOLEAN
      --  Delete (one-level) subdirectory dirname on disk.
      --  Nested deletions support and semantics are not guaranteed for 
      --  portability reasons.
      --  Return true if succeeded, false otherwise.
      --  In case of success, update has been successfully done.

      require
         is_subdirectory(index_of(dirname))


end of BASIC_DIRECTORY