class interface DIRECTORY
--
-- Tools for file-system directory handling.
--
-- Clean hight-level facade for class BASIC_DIRECTORY.
--
creation
connect_to (new_path: STRING)
require
not new_path.empty
feature(s) from DIRECTORY
is_connected: BOOLEAN
feature(s) from DIRECTORY
-- Creation / Modification :
connect_to (new_path: STRING)
require
not new_path.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
valid_index (index: INTEGER): BOOLEAN
ensure
Result = index.in_range(1,count)
path: STRING
require
is_connected
name (index: INTEGER): STRING
-- Return the name of entry (file or subdirectory) at index.
require
is_connected;
valid_index(index)
ensure
has(Result)
has (entry_name: STRING): BOOLEAN
-- Does Current contain the entry_name (file or subdirectory) ?
require
is_connected;
not entry_name.empty
end of DIRECTORY