class DIRECTORY

All features

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

Direct parents

non-conformant parents

ANY

Summary

creation features

exported features

Disk access:

Access:

File access:

Details

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
  • directory_path /= path

ensure

  • not last_scan_status implies is_empty
  • path.is_equal(directory_path)
  • path /= directory_path

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

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.

basic_directory: BASIC_DIRECTORY

Provide low level access to directories.

name_list: FAST_ARRAY [E_][STRING]

Actual list of entries (files or subdirectories)..

make

Make a new not assigned one.

ensure

  • is_empty

init (suggested_path_capacity: INTEGER)

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
  • directory_path /= path

ensure

  • not last_scan_status implies is_empty
  • path.is_equal(directory_path)
  • path /= directory_path

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

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

connect_to_file (file: FILE, filename: STRING)

Connect the file to the operating system file given by its filename.

require

  • file /= Void

path_buffer: STRING

Class invariant