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