indexing
description: "Directories, in the Unix sense, with creation and exploration features"
class interface
DIRECTORY
create
make (dn: STRING)
-- Create directory object for the directory
-- of name dn.
require
string_exists: dn /= void
make_open_read (dn: STRING)
-- Create directory object for the directory
-- of name dn and open it for reading.
require
string_exists: dn /= void
feature -- Initialization
create_dir
-- Create a physical directory.
require
physical_not_exists: not exists
make (dn: STRING)
-- Create directory object for the directory
-- of name dn.
require
string_exists: dn /= void
make_open_read (dn: STRING)
-- Create directory object for the directory
-- of name dn and open it for reading.
require
string_exists: dn /= void
feature -- Access
change_name (new_name: STRING)
-- Change file name to new_name
require
not_new_name_void: new_name /= void;
file_exists: exists
ensure
name_changed: name.is_equal (new_name)
close
-- Close directory.
require
is_open: not is_closed
has_entry (entry_name: STRING): BOOLEAN
-- Has directory the entry entry_name?
-- The use of dir_temp is required not
-- to change the position in the current
-- directory entries list.
require
string_exists: entry_name /= void
name: STRING
-- Directory name
open_read
-- Open directory name for reading.
readentry
-- Read next directory entry;
-- make result available in lastentry.
-- Make result void if all entries have been read.
require
is_opened: not is_closed
start
-- Go to first entry of directory.
require
is_opened: not is_closed
feature -- Measurement
count: INTEGER
-- Number of entries in directory.
require
directory_exists: exists
feature -- Status report
empty: BOOLEAN
-- Is directory empty?
require
directory_exists: exists
exists: BOOLEAN
-- Does the directory exist?
is_closed: BOOLEAN
-- Is current directory closed?
is_executable: BOOLEAN
-- Is the directory executable?
require
directory_exists: exists
is_readable: BOOLEAN
-- Is the directory readable?
require
directory_exists: exists
is_writable: BOOLEAN
-- Is the directory writable?
require
directory_exists: exists
lastentry: STRING
-- Last entry read by readentry
feature -- Removal
delete
-- Delete directory if empty
require
directory_exists: exists;
empty_directory: empty
dispose
-- Ensure this medium is closed when garbage collected.
feature -- Conversion
linear_representation: ARRAYED_LIST [STRING]
-- The entries, in sequential format.
end -- class DIRECTORY